From 20344cfe94aa5ba4d4f249ccc3ff7dc6a8965c70 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 13 Mar 2026 08:41:09 +0100 Subject: [PATCH 1/2] [refman] Remove unused bibliography --- .gitignore | 1 - .../stdlib-refman-html/default.nix | 2 +- doc/README.md | 3 +- doc/sphinx/biblio.bib | 677 ------------------ doc/sphinx/conf.py | 4 - doc/sphinx/index.html.rst | 1 - doc/sphinx/index.latex.rst | 1 - doc/sphinx/zebibliography.html.rst | 17 - doc/sphinx/zebibliography.latex.rst | 6 - doc/tools/rocqrst/checkdeps.py | 5 - 10 files changed, 2 insertions(+), 715 deletions(-) delete mode 100644 doc/sphinx/biblio.bib delete mode 100644 doc/sphinx/zebibliography.html.rst delete mode 100644 doc/sphinx/zebibliography.latex.rst diff --git a/.gitignore b/.gitignore index cf23c7c455..84f86a2ac4 100644 --- a/.gitignore +++ b/.gitignore @@ -109,7 +109,6 @@ doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png doc/sphinx/index.rst -doc/sphinx/zebibliography.rst doc/corelib/Library.out doc/corelib/Library.ps doc/corelib/Library.coqdoc.tex diff --git a/.nix/rocq-overlays/stdlib-refman-html/default.nix b/.nix/rocq-overlays/stdlib-refman-html/default.nix index 5c2361a85b..bdf9ed39ac 100644 --- a/.nix/rocq-overlays/stdlib-refman-html/default.nix +++ b/.nix/rocq-overlays/stdlib-refman-html/default.nix @@ -9,7 +9,7 @@ rocqPackages.lib.overrideRocqDerivation { # Sphinx doc dependencies (python312.withPackages (ps: [ ps.sphinx ps.sphinx-rtd-theme ps.pexpect ps.beautifulsoup4 - (ps.antlr4-python3-runtime.override {antlr4 = antlr4_9;}) ps.sphinxcontrib-bibtex ])) + (ps.antlr4-python3-runtime.override {antlr4 = antlr4_9;}) ])) antlr4_9 ]; diff --git a/doc/README.md b/doc/README.md index f2f8d991cd..2ed9ef3024 100644 --- a/doc/README.md +++ b/doc/README.md @@ -38,13 +38,12 @@ Otherwise, you need to install (in another way) Python 3, and the following Pyth - beautifulsoup4 >= 4.8.2 - antlr4-python3-runtime >= 4.7.1 & <= 4.9.3 - pexpect >= 4.6.0 - - sphinxcontrib-bibtex >= 0.4.2 For instance, on Debian / Ubuntu, you can install pip and setuptools with `apt install python3-pip python3-setuptools` on Debian / Ubuntu then run: pip3 install sphinx sphinx-rtd-theme beautifulsoup4 \ - antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex + antlr4-python3-runtime==4.7.1 pexpect You can check the dependencies using the `doc/tools/rocqrst/checkdeps.py` script. diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib deleted file mode 100644 index a68c07d918..0000000000 --- a/doc/sphinx/biblio.bib +++ /dev/null @@ -1,677 +0,0 @@ -@String{jfp = "Journal of Functional Programming"} -@String{lncs = "Lecture Notes in Computer Science"} -@String{lnai = "Lecture Notes in Artificial Intelligence"} -@String{SV = "{Springer-Verlag}"} - -@InCollection{Asp00, - Title = {Proof General: A Generic Tool for Proof Development}, - Author = {Aspinall, David}, - Booktitle = {Tools and Algorithms for the Construction and - Analysis of Systems, {TACAS} 2000}, - Publisher = {Springer Berlin Heidelberg}, - Year = {2000}, - Editor = {Graf, Susanne and Schwartzbach, Michael}, - Pages = {38--43}, - Series = {Lecture Notes in Computer Science}, - Volume = {1785}, - Doi = {10.1007/3-540-46419-0_3}, - ISBN = {978-3-540-67282-1}, -} - -@Book{Bar81, - author = {H.P. Barendregt}, - publisher = {North-Holland}, - title = {The Lambda Calculus its Syntax and Semantics}, - year = {1981} -} - -@InProceedings{Bou97, - title = {Using reflection to build efficient and certified decision procedure -s}, - author = {S. Boutin}, - booktitle = {TACS'97}, - editor = {Martin Abadi and Takahashi Ito}, - publisher = SV, - series = lncs, - volume = 1281, - year = {1997} -} - -@Article{Bru72, - author = {N.J. de Bruijn}, - journal = {Indag. Math.}, - title = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, - volume = {34}, - year = {1972} -} - -@inproceedings{CH85, - title={Constructions: a higher order proof system for mechanizing mathematics}, - author={Coquand, Thierry and Huet, Gérard}, - booktitle={European Conference on Computer Algebra}, - pages={151--184}, - year={1985}, - issn = {1611-3349}, - doi = {10.1007/3-540-15983-5_13}, - url = {http://dx.doi.org/10.1007/3-540-15983-5_13}, - isbn = 9783540396840, - publisher = {Springer Berlin Heidelberg} -} - -@techreport{CH88 - TITLE = {{The calculus of constructions}}, - AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, - URL = {https://hal.inria.fr/inria-00076024}, - NUMBER = {RR-0530}, - INSTITUTION = {{INRIA}}, - YEAR = {1986}, - MONTH = May, - PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf}, - HAL_ID = {inria-00076024}, - HAL_VERSION = {v1}, -} - -@techreport{CH87, - TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}}, - AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, - URL = {https://hal.inria.fr/inria-00076039}, - NUMBER = {RR-0515}, - INSTITUTION = {{INRIA}}, - YEAR = {1986}, - MONTH = Apr, - PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf}, - HAL_ID = {inria-00076039}, - HAL_VERSION = {v1}, -} - -@techreport{C90, - TITLE = {{Metamathematical investigations of a calculus of constructions}}, - AUTHOR = {Coquand, T.}, - URL = {https://hal.inria.fr/inria-00075471}, - NUMBER = {RR-1088}, - INSTITUTION = {{INRIA}}, - YEAR = {1989}, - MONTH = Sep, - PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf}, - HAL_ID = {inria-00075471}, - HAL_VERSION = {v1}, -} - -@PhDThesis{Coq85, - author = {Th. Coquand}, - month = jan, - school = {Universit\'e Paris~7}, - title = {Une Th\'eorie des Constructions}, - year = {1985} -} - -@InProceedings{Coq86, - author = {Th. Coquand}, - address = {Cambridge, MA}, - booktitle = {Symposium on Logic in Computer Science}, - publisher = {IEEE Computer Society Press}, - title = {{An Analysis of Girard's Paradox}}, - year = {1986} -} - -@InProceedings{Coq92, - author = {Th. Coquand}, - title = {{Pattern Matching with Dependent Types}}, - year = {1992}, - booktitle = {Proceedings of the 1992 Workshop on Types for Proofs and Programs} -} - -@InProceedings{DBLP:conf/types/CornesT95, - author = {Cristina Cornes and - Delphine Terrasse}, - title = {Automating Inversion of Inductive Predicates in Coq}, - booktitle = {TYPES}, - year = {1995}, - pages = {85-104}, - crossref = {DBLP:conf/types/1995}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@inproceedings{CP90, - title={Inductively defined types}, - author={Coquand, Thierry and Paulin, Christine}, - booktitle={COLOG-88}, - pages={50--66}, - year={1990}, - issn = {1611-3349}, - doi = {10.1007/3-540-52335-9_47}, - url = {http://dx.doi.org/10.1007/3-540-52335-9_47}, - isbn = 9783540469636, - publisher = {Springer Berlin Heidelberg} -} - -@Book{Cur58, - author = {Haskell B. Curry and Robert Feys and William Craig}, - title = {Combinatory Logic}, - volume = 1, - publisher = "North-Holland", - year = 1958, - note = {{\S{9E}}}, -} - -@Article{CSlessadhoc, - author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, - title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, - journal = {SIGPLAN Not.}, - issue_date = {September 2011}, - volume = {46}, - number = {9}, - month = sep, - year = {2011}, - issn = {0362-1340}, - pages = {163--175}, - numpages = {13}, - url = {http://doi.acm.org/10.1145/2034574.2034798}, - doi = {10.1145/2034574.2034798}, - acmid = {2034798}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, -} - -@InProceedings{CSwcu, - hal_id = {hal-00816703}, - url = {http://hal.inria.fr/hal-00816703}, - title = {{Canonical Structures for the working Coq user}}, - author = {Mahboubi, Assia and Tassi, Enrico}, - booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, - publisher = {Springer}, - pages = {19-34}, - address = {Rennes, France}, - volume = {7998}, - editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, - series = {LNCS }, - doi = {10.1007/978-3-642-39634-2_5}, - year = {2013}, -} - -@InProceedings{Del00, - author = {Delahaye, D.}, - title = {A {T}actic {L}anguage for the {S}ystem {Coq}}, - booktitle = {Proceedings of Logic for Programming and Automated Reasoning - (LPAR), Reunion Island}, - publisher = SV, - series = LNCS, - volume = {1955}, - pages = {85--95}, - month = {November}, - year = {2000}, - url = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf} -} - -@Article{Dyc92, - author = {Roy Dyckhoff}, - journal = {The Journal of Symbolic Logic}, - month = sep, - number = {3}, - title = {Contraction-free sequent calculi for intuitionistic logic}, - volume = {57}, - year = {1992} -} - -@Book{Fourier, - author = {Jean-Baptiste-Joseph Fourier}, - publisher = {Gauthier-Villars}, - title = {Fourier's method to solve linear - inequations/equations systems.}, - year = {1890} -} - -@article{Gilbert:POPL2019, - author = {Gilbert, Ga\"{e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas}, - title = {{Definitional Proof Irrelevance Without K}}, - journal = {Proc. ACM Program. Lang.}, - issue_date = {January 2019}, - volume = {3}, - number = {POPL}, - year = {2019}, - issn = {2475-1421}, - pages = {3:1--3:28}, - articleno = {3}, - numpages = {28}, - url = {http://doi.acm.org/10.1145/3290316}, - acmid = {3290316}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {proof assistants, proof irrelevance, type theory}, -} - -@InProceedings{Gim94, - author = {E. Gim\'enez}, - booktitle = {Types'94 : Types for Proofs and Programs}, - note = {Extended version in LIP research report 95-07, ENS Lyon}, - publisher = SV, - series = LNCS, - title = {Codifying guarded definitions with recursive schemes}, - volume = {996}, - year = {1994} -} - -@TechReport{Gim98, - author = {E. Gim\'enez}, - title = {A Tutorial on Recursive Types in Coq}, - institution = {INRIA}, - year = 1998, - month = mar -} - -@Unpublished{GimCas05, - author = {E. Gim\'enez and P. Cast\'eran}, - title = {A Tutorial on [Co-]Inductive Types in Coq}, - institution = {INRIA}, - year = 2005, - month = jan, - note = {available at \url{http://coq.inria.fr/doc}} -} - -@InProceedings{Gimenez95b, - author = {E. Gim\'enez}, - booktitle = {Workshop on Types for Proofs and Programs}, - series = LNCS, - number = {1158}, - pages = {135-152}, - title = {An application of co-Inductive types in Coq: - verification of the Alternating Bit Protocol}, - editorS = {S. Berardi and M. Coppo}, - publisher = SV, - year = {1995} -} - -@Book{Gir89, - author = {J.-Y. Girard and Y. Lafont and P. Taylor}, - publisher = {Cambridge University Press}, - series = {Cambridge Tracts in Theoretical Computer Science 7}, - title = {Proofs and Types}, - year = {1989} -} - -@InCollection{How80, - author = {W.A. Howard}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - note = {Unpublished 1969 Manuscript}, - publisher = {Academic Press}, - title = {The Formulae-as-Types Notion of Constructions}, - year = {1980} -} - -@inproceedings{H88, - title={Induction principles formalized in the Calculus of Constructions}, - author={Huet, G{\'e}rard}, - booktitle={Programming of Future Generation Computers. Elsevier Science}, - year={1988}, - issn = {1611-3349}, - doi = {10.1007/3-540-17660-8_62}, - url = {http://dx.doi.org/10.1007/3-540-17660-8_62}, - isbn = 9783540477464, - publisher = {Springer Berlin Heidelberg} -} - -@InProceedings{H89, - author = {G. Huet}, - booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, - editor = {R. Narasimhan}, - publisher = {World Scientific Publishing}, - title = {{The Constructive Engine}}, - year = {1989} -} - -@Article{LeeWerner11, - author = {Gyesik Lee and - Benjamin Werner}, - title = {Proof-irrelevant model of {CC} with predicative induction - and judgmental equality}, - journal = {Logical Methods in Computer Science}, - volume = {7}, - number = {4}, - year = {2011}, - ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@TechReport{Leroy90, - author = {X. Leroy}, - title = {The {ZINC} experiment: an economical implementation of the {ML} language}, - institution = {INRIA}, - number = {117}, - year = {1990} -} - -@InProceedings{Let02, - author = {P. Letouzey}, - title = {A New Extraction for Coq}, - booktitle = {TYPES}, - year = 2002, - crossref = {DBLP:conf/types/2002}, - url = {http://www.irif.fr/~letouzey/download/extraction2002.pdf} -} - -@InProceedings{Luttik97specificationof, - author = {Sebastiaan P. Luttik and Eelco Visser}, - booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, - publisher = SV, - title = {Specification of Rewriting Strategies}, - year = {1997} -} - -@inproceedings{Visser98, - author = {Eelco Visser and - Zine{-}El{-}Abidine Benaissa and - Andrew P. Tolmach}, - title = {Building Program Optimizers with Rewriting Strategies}, - booktitle = {ICFP}, - pages = {13--26}, - year = {1998}, -} - -@inproceedings{Visser01, - author = {Eelco Visser}, - title = {Stratego: {A} Language for Program Transformation Based on Rewriting - Strategies}, - booktitle = {RTA}, - pages = {357--362}, - year = {2001}, - series = {LNCS}, - volume = {2051}, -} - -@InProceedings{DBLP:conf/types/McBride00, - author = {Conor McBride}, - title = {Elimination with a Motive}, - booktitle = {TYPES}, - year = {2000}, - pages = {197-216}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, - crossref = {DBLP:conf/types/2000}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@InProceedings{Moh93, - author = {C. Paulin-Mohring}, - booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications}, - editor = {M. Bezem and J.-F. Groote}, - note = {Also LIP research report 92-49, ENS Lyon}, - number = {664}, - publisher = SV, - series = {LNCS}, - title = {{Inductive Definitions in the System Coq - Rules and Properties}}, - year = {1993} -} - -@MastersThesis{Mun94, - author = {C. Muñoz}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, - year = {1994} -} - -@Article{Myers, - author = {Eugene Myers}, - title = {An {O(ND)} difference algorithm and its variations}, - journal = {Algorithmica}, - volume = {1}, - number = {2}, - year = {1986}, - bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446}, - url = {http://www.xmailserver.org/diff2.pdf} -} - -@inproceedings{P86, - title={Algorithm development in the calculus of constructions}, - author={Mohring, Christine}, - booktitle={LICS}, - pages={84--91}, - year={1986} -} - -@inproceedings{P89, - title={Extracting $\Omega$'s programs from proofs in the calculus of constructions}, - author={Paulin-Mohring, Christine}, - booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, - pages={89--104}, - year={1989}, - doi = {10.1145/75277.75285}, - url = {http://dx.doi.org/10.1145/75277.75285}, - isbn = 0897912942, - organization = {ACM Press} -} - -@inproceedings{P93, - title={Inductive definitions in the system coq rules and properties}, - author={Paulin-Mohring, Christine}, - booktitle={International Conference on Typed Lambda Calculi and Applications}, - pages={328--345}, - year={1993}, - doi = {10.1007/bfb0037116}, - url = {http://dx.doi.org/10.1007/bfb0037116}, - isbn = 3540565175, - organization = {Springer-Verlag} -} - -@inproceedings{PP90, - title={Inductively defined types in the Calculus of Constructions}, - author={Pfenning, Frank and Paulin-Mohring, Christine}, - booktitle={International Conference on Mathematical Foundations of Programming Semantics}, - pages={209--228}, - year={1989}, - doi = {10.1007/bfb0040259}, - url = {http://dx.doi.org/10.1007/bfb0040259}, - isbn = 0387973753, - organization = {Springer-Verlag} -} - -@InProceedings{Parent95b, - author = {C. Parent}, - booktitle = {{Mathematics of Program Construction'95}}, - publisher = SV, - series = {LNCS}, - title = {{Synthesizing proofs from programs in -the Calculus of Inductive Constructions}}, - volume = {947}, - year = {1995} -} - -@InProceedings{Pit16, - Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, - Author = {Pit-Claudel, Clément and Courtieu, Pierre}, - Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, - Year = {2016}, - Month = jan, - Doi = {10.5281/zenodo.44331}, -} - -@Book{RC95, - author = {di~Cosmo, R.}, - title = {Isomorphisms of Types: from $\lambda$-calculus to information - retrieval and language design}, - series = {Progress in Theoretical Computer Science}, - publisher = {Birkhauser}, - year = {1995}, - note = {ISBN-0-8176-3763-X} -} - -@Article{Rushby98, - title = {Subtypes for Specifications: Predicate Subtyping in - {PVS}}, - author = {John Rushby and Sam Owre and N. Shankar}, - journal = {IEEE Transactions on Software Engineering}, - pages = {709--720}, - volume = 24, - number = 9, - month = sep, - year = 1998 -} - -@InProceedings{sozeau06, - author = {Matthieu Sozeau}, - title = {Subset Coercions in {C}oq}, - year = {2007}, - booktitle = {TYPES'06}, - pages = {237-252}, - volume = {4502}, - publisher = "Springer", - series = {LNCS} -} - -@InProceedings{sozeau08, - Author = {Matthieu Sozeau and Nicolas Oury}, - booktitle = {TPHOLs'08}, - Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf}, - Title = {{F}irst-{C}lass {T}ype {C}lasses}, - Year = {2008}, -} - -@InProceedings{sugar, - author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, - title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, - booktitle = { Proceedings of the ISSAC'91, ACM Press}, - year = {1991}, - pages = {5--4}, - publisher = {} -} - -@PhDThesis{Wer94, - author = {B. Werner}, - school = {Universit\'e Paris 7}, - title = {Une th\'eorie des constructions inductives}, - type = {Th\`ese de Doctorat}, - year = {1994} -} - -@InProceedings{CompiledStrongReduction, - author = {Benjamin Gr{\'{e}}goire and - Xavier Leroy}, - editor = {Mitchell Wand and - Simon L. Peyton Jones}, - title = {A compiled implementation of strong reduction}, - booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference - on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania, - USA, October 4-6, 2002.}, - pages = {235--246}, - publisher = {{ACM}}, - year = {2002}, - url = {http://doi.acm.org/10.1145/581478.581501}, - doi = {10.1145/581478.581501}, - timestamp = {Tue, 11 Jun 2013 13:49:16 +0200}, - biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} - -@InProceedings{FullReduction, - author = {Mathieu Boespflug and - Maxime D{\'{e}}n{\`{e}}s and - Benjamin Gr{\'{e}}goire}, - editor = {Jean{-}Pierre Jouannaud and - Zhong Shao}, - title = {Full Reduction at Full Throttle}, - booktitle = {Certified Programs and Proofs - First International Conference, {CPP} - 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings}, - series = {Lecture Notes in Computer Science}, - volume = {7086}, - pages = {362--377}, - publisher = {Springer}, - year = {2011}, - url = {http://dx.doi.org/10.1007/978-3-642-25379-9_26}, - doi = {10.1007/978-3-642-25379-9_26}, - timestamp = {Thu, 17 Nov 2011 13:33:48 +0100}, - biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} - -@inproceedings{MilnerPrincipalTypeSchemes, - author = {Damas, Luis and Milner, Robin}, - title = {Principal Type-schemes for Functional Programs}, - booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, - series = {POPL '82}, - year = {1982}, - isbn = {0-89791-065-6}, - location = {Albuquerque, New Mexico}, - pages = {207--212}, - numpages = {6}, - url = {http://doi.acm.org/10.1145/582153.582176}, - doi = {10.1145/582153.582176}, - acmid = {582176}, - publisher = {ACM}, - address = {New York, NY, USA}, -} - -@techreport{abel19:failur_normal_impred_type_theor, - author = {Andreas Abel AND Thierry Coquand}, - title = {{Failure of Normalization in Impredicative Type - Theory with Proof-Irrelevant Propositional - Equality}}, - year = 2019, - institution = {Chalmers and Gothenburg University}, -} - -@inproceedings{ConchonFilliatre07wml, - author = {Sylvain Conchon and Jean-Christophe Filliâtre}, - title = {A Persistent Union-Find Data Structure}, - booktitle = {ACM SIGPLAN Workshop on ML}, - publisher = {ACM Press}, - pages = {37--45}, - year = 2007, - address = {Freiburg, Germany}, - month = {October}, - topics = {team, lri}, - type_publi = {icolcomlec}, - type_digiteo = {conf_isbn}, - x-pdf = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, - url = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, - abstract = { The problem of disjoint sets, also known as union-find, - consists in maintaining a partition of a finite set within a data - structure. This structure provides two operations: a function find - returning the class of an element and a function union merging two - classes. An optimal and imperative solution is known since 1975. - However, the imperative nature of this data structure may be a - drawback when it is used in a backtracking algorithm. This paper - details the implementation of a persistent union-find data structure - as efficient as its imperative counterpart. To achieve this result, - our solution makes heavy use of imperative features and thus it is a - significant example of a data structure whose side effects are - safely hidden behind a persistent interface. To strengthen this - last claim, we also detail a formalization using the Coq proof - assistant which shows both the correctness of our solution and its - observational persistence. }, - x-equipes = {demons PROVAL}, - x-type = {article}, - x-support = {actes_aux}, - x-cle-support = {ML} -} - -@phdthesis{Zimmermann19, - author = {Th{\'{e}}o Zimmermann}, - title = {Challenges in the collaborative evolution of a proof language and - its ecosystem.}, - school = {Université de Paris, France}, - year = {2019}, - url = {https://tel.archives-ouvertes.fr/tel-02451322}, - timestamp = {Tue, 21 Jul 2020 00:40:54 +0200}, - biburl = {https://dblp.org/rec/phd/hal/Zimmermann19.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@article{TotR21, - author = {Cockx, Jesper and Tabareau, Nicolas and Winterhalter, Th\'{e}o}, - title = {The Taming of the Rew: A Type Theory with Computational Assumptions}, - year = {2021}, - issue_date = {January 2021}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {5}, - number = {POPL}, - url = {https://doi.org/10.1145/3434341}, - doi = {10.1145/3434341}, - abstract = {Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logical principles in those systems, it is common to appeal to axioms to postulate their existence. However, one can only postulate the bare existence of an axiom, not its computational behaviour. Instead, users are forced to postulate equality proofs and appeal to them explicitly to simplify expressions, making axioms dramatically more complicated to work with than built-in primitives. On the other hand, the equality reflection rule from extensional type theory solves these problems by collapsing computation and equality, at the cost of having no practical type checking algorithm. This paper introduces Rewriting Type Theory (RTT), a type theory where it is possible to add computational assumptions in the form of rewrite rules. Rewrite rules go beyond the computational capabilities of intensional type theory, but in contrast to extensional type theory, they are applied automatically so type checking does not require input from the user. To ensure type soundness of RTT—as well as effective type checking—we provide a framework where confluence of user-defined rewrite rules can be checked modularly and automatically, and where adding new rewrite rules is guaranteed to preserve subject reduction. The properties of RTT have been formally verified using the MetaCoq framework and an implementation of rewrite rules is already available in the Agda proof assistant.}, - journal = {Proc. ACM Program. Lang.}, - month = {jan}, - articleno = {60}, - numpages = {29}, - keywords = {termination, dependent types, rewriting theory, confluence, type theory} -} diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 8fcf8a03bd..ecf4b93bc4 100644 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -56,7 +56,6 @@ 'sphinx.ext.ifconfig', 'sphinx.ext.mathjax', 'sphinx.ext.todo', - 'sphinxcontrib.bibtex', 'rocqrst.rocqdomain' ] @@ -497,6 +496,3 @@ def setup(app): # navtree options navtree_shift = True - -# since sphinxcontrib-bibtex version 2 we need this -bibtex_bibfiles = [ "biblio.bib" ] diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index b06c179ead..1711fd3a36 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -20,6 +20,5 @@ Contents :caption: Appendix changes - zebibliography .. include:: license.rst diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 19710d5351..936b264f00 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -25,4 +25,3 @@ Appendix .. toctree:: changes - zebibliography diff --git a/doc/sphinx/zebibliography.html.rst b/doc/sphinx/zebibliography.html.rst deleted file mode 100644 index 756edd5482..0000000000 --- a/doc/sphinx/zebibliography.html.rst +++ /dev/null @@ -1,17 +0,0 @@ -.. There are multiple issues with sphinxcontrib-bibtex that we have to work around: - - The list of cited entries is computed right after encountering - `.. bibliography`, so the file containing that command has to come last - alphabetically: - https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents - - `.. bibliography::` puts the bibliography on its own page with its own - title in LaTeX, but includes it inline without a title in HTML: - https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends - -.. _bibliography: - -============== - Bibliography -============== - -.. bibliography:: biblio.bib - :cited: diff --git a/doc/sphinx/zebibliography.latex.rst b/doc/sphinx/zebibliography.latex.rst deleted file mode 100644 index 2c0396f1c9..0000000000 --- a/doc/sphinx/zebibliography.latex.rst +++ /dev/null @@ -1,6 +0,0 @@ -.. See zebibliography.html.rst for details - -.. _bibliography: - -.. bibliography:: biblio.bib - :cited: diff --git a/doc/tools/rocqrst/checkdeps.py b/doc/tools/rocqrst/checkdeps.py index 12cf418077..acebe068a5 100644 --- a/doc/tools/rocqrst/checkdeps.py +++ b/doc/tools/rocqrst/checkdeps.py @@ -45,9 +45,4 @@ def report_missing_deps(): except: missing_dep('beautifulsoup4') -try: - import sphinxcontrib.bibtex -except: - missing_dep('sphinxcontrib-bibtex') - report_missing_deps() From fb636a8c650adbc5a05ffc5a71262307cefa31af Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 12 Mar 2026 15:53:50 +0100 Subject: [PATCH 2/2] [CI] Update Nix toolbox --- .github/workflows/nix-action-rocq-9.1.yml | 157 ++++++++++-------- .github/workflows/nix-action-rocq-9.2.yml | 145 ++++------------ .github/workflows/nix-action-rocq-master.yml | 140 ++++------------ .nix/config.nix | 49 +++--- .nix/coq-nix-toolbox.nix | 2 +- .nix/rocq-overlays/rocq-elpi-test/default.nix | 9 +- 6 files changed, 184 insertions(+), 318 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 334af01b0c..107ad041d3 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -327,6 +327,7 @@ jobs: QuickChick: needs: - coq + - mathcomp-boot - ExtLib - simple-io runs-on: ubuntu-latest @@ -381,6 +382,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: ExtLib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -462,7 +467,6 @@ jobs: - coq - Cheerios - InfSeqExt - - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -800,6 +804,7 @@ jobs: autosubst: needs: - coq + - mathcomp-boot - stdlib runs-on: ubuntu-latest steps: @@ -853,6 +858,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1500,6 +1509,7 @@ jobs: needs: - coq - stdlib + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1556,6 +1566,10 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1627,7 +1641,6 @@ jobs: deriving: needs: - coq - - mathcomp-ssreflect - stdlib runs-on: ubuntu-latest steps: @@ -1824,6 +1837,7 @@ jobs: fcsl-pcm: needs: - coq + - mathcomp-algebra - stdlib runs-on: ubuntu-latest steps: @@ -1877,6 +1891,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2494,7 +2512,7 @@ jobs: mathcomp-algebra-tactics: needs: - coq - - mathcomp-ssreflect + - mathcomp-algebra - coq-elpi - mathcomp-zify runs-on: ubuntu-latest @@ -2553,6 +2571,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq-elpi' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2569,6 +2591,7 @@ jobs: needs: - coq - mathcomp-reals + - mathcomp-field - mathcomp-bigenough - hierarchy-builder runs-on: ubuntu-latest @@ -2627,6 +2650,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-reals" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2720,7 +2747,8 @@ jobs: "rocq-9.1" --argstr job "mathcomp-analysis-stdlib" mathcomp-bigenough: needs: - - coq + - rocq-core + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2770,9 +2798,13 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2913,7 +2945,7 @@ jobs: mathcomp-classical: needs: - coq - - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-finmap - hierarchy-builder runs-on: ubuntu-latest @@ -2972,6 +3004,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3124,7 +3160,8 @@ jobs: "rocq-9.1" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -3174,9 +3211,13 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3462,69 +3503,11 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-ssreflect) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2> err > - out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-ssreflect" mathcomp-word: needs: - coq - - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup - stdlib runs-on: ubuntu-latest steps: @@ -3578,10 +3561,18 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3593,6 +3584,9 @@ jobs: mathcomp-zify: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-fingroup - stdlib runs-on: ubuntu-latest steps: @@ -3646,6 +3640,18 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4323,6 +4329,7 @@ jobs: needs: - coq - aac-tactics + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -4379,6 +4386,10 @@ jobs: name: 'Building/fetching previous CI target: aac-tactics' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "aac-tactics" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5010,7 +5021,7 @@ jobs: "rocq-9.1" --argstr job "stdlib-refman-html" stdpp: needs: - - coq + - rocq-core - stdlib runs-on: ubuntu-latest steps: @@ -5061,9 +5072,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 24e8e43739..eb407baf75 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -467,7 +467,6 @@ jobs: - coq - Cheerios - InfSeqExt - - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1642,7 +1641,6 @@ jobs: deriving: needs: - coq - - mathcomp-ssreflect - stdlib runs-on: ubuntu-latest steps: @@ -2370,7 +2368,7 @@ jobs: "rocq-9.2" --argstr job "math-classes" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -2422,9 +2420,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2439,7 +2437,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder @@ -2492,9 +2490,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2514,7 +2512,6 @@ jobs: mathcomp-algebra-tactics: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - coq-elpi - mathcomp-zify @@ -2750,7 +2747,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-analysis-stdlib" mathcomp-bigenough: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -2801,9 +2798,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2814,7 +2811,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -2865,9 +2862,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2878,7 +2875,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-boot" mathcomp-character: needs: - - coq + - rocq-core - mathcomp-field - hierarchy-builder runs-on: ubuntu-latest @@ -2930,9 +2927,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2948,7 +2945,6 @@ jobs: mathcomp-classical: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - mathcomp-finmap - hierarchy-builder @@ -3026,7 +3022,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-classical" mathcomp-field: needs: - - coq + - rocq-core - mathcomp-solvable - hierarchy-builder runs-on: ubuntu-latest @@ -3078,9 +3074,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3095,7 +3091,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-field" mathcomp-fingroup: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -3147,9 +3143,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3164,7 +3160,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -3215,9 +3211,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3228,7 +3224,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-finmap" mathcomp-order: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -3280,9 +3276,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3440,7 +3436,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-reals-stdlib" mathcomp-solvable: needs: - - coq + - rocq-core - mathcomp-algebra - hierarchy-builder runs-on: ubuntu-latest @@ -3492,9 +3488,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3507,85 +3503,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - needs: - - coq - - mathcomp-boot - - mathcomp-order - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-ssreflect) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2> err > - out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-boot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "mathcomp-boot" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-order' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "mathcomp-order" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "mathcomp-ssreflect" mathcomp-word: needs: - coq - mathcomp-algebra - - mathcomp-ssreflect - mathcomp-fingroup - stdlib runs-on: ubuntu-latest @@ -4883,7 +4804,7 @@ jobs: "rocq-9.2" --argstr job "stdlib-warnings" stdpp: needs: - - coq + - rocq-core - stdlib runs-on: ubuntu-latest steps: @@ -4934,9 +4855,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 7530583666..2f36486b45 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -600,7 +600,6 @@ jobs: - coq - Cheerios - InfSeqExt - - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1332,7 +1331,6 @@ jobs: category-theory: needs: - coq - - mathcomp-ssreflect - equations runs-on: ubuntu-latest steps: @@ -2312,7 +2310,6 @@ jobs: deriving: needs: - coq - - mathcomp-ssreflect - stdlib runs-on: ubuntu-latest steps: @@ -3498,7 +3495,7 @@ jobs: "rocq-master" --argstr job "math-classes" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -3550,9 +3547,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3567,7 +3564,7 @@ jobs: "rocq-master" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder @@ -3620,9 +3617,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3642,7 +3639,6 @@ jobs: mathcomp-algebra-tactics: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - coq-elpi - mathcomp-zify @@ -3878,7 +3874,7 @@ jobs: "rocq-master" --argstr job "mathcomp-analysis-stdlib" mathcomp-bigenough: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -3929,9 +3925,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3942,7 +3938,7 @@ jobs: "rocq-master" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -3993,9 +3989,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4006,7 +4002,7 @@ jobs: "rocq-master" --argstr job "mathcomp-boot" mathcomp-character: needs: - - coq + - rocq-core - mathcomp-field - hierarchy-builder runs-on: ubuntu-latest @@ -4058,9 +4054,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4076,7 +4072,6 @@ jobs: mathcomp-classical: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - mathcomp-finmap - hierarchy-builder @@ -4154,7 +4149,7 @@ jobs: "rocq-master" --argstr job "mathcomp-classical" mathcomp-field: needs: - - coq + - rocq-core - mathcomp-solvable - hierarchy-builder runs-on: ubuntu-latest @@ -4206,9 +4201,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4223,7 +4218,7 @@ jobs: "rocq-master" --argstr job "mathcomp-field" mathcomp-fingroup: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -4275,9 +4270,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4292,7 +4287,7 @@ jobs: "rocq-master" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -4343,9 +4338,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4356,7 +4351,7 @@ jobs: "rocq-master" --argstr job "mathcomp-finmap" mathcomp-order: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -4408,9 +4403,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4568,7 +4563,7 @@ jobs: "rocq-master" --argstr job "mathcomp-reals-stdlib" mathcomp-solvable: needs: - - coq + - rocq-core - mathcomp-algebra - hierarchy-builder runs-on: ubuntu-latest @@ -4620,9 +4615,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4635,85 +4630,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - needs: - - coq - - mathcomp-boot - - mathcomp-order - - hierarchy-builder - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-ssreflect) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2> err - > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-boot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-boot" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-order' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-order" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-ssreflect" mathcomp-word: needs: - coq - mathcomp-algebra - - mathcomp-ssreflect - mathcomp-fingroup - stdlib runs-on: ubuntu-latest diff --git a/.nix/config.nix b/.nix/config.nix index e4892cf5e3..3d0dc0c4e5 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -97,6 +97,22 @@ with builtins; with (import {}).lib; ## Run on push on following branches (default [ "master" ]) # push-branches = [ "master" "branch2" ]; + rocq-master = [ + "bignums" + "rocq-elpi" + "rocq-elpi-test" + "hierarchy-builder" + "mathcomp" + "mathcomp-algebra" + "mathcomp-bigenough" + "mathcomp-boot" + "mathcomp-character" + "mathcomp-field" + "mathcomp-fingroup" + "mathcomp-finmap" + "mathcomp-order" + "mathcomp-solvable" + ]; master = [ "aac-tactics" "argosy" @@ -140,21 +156,10 @@ with builtins; with (import {}).lib; "itree-io" "json" "kami" - "mathcomp" - "mathcomp-algebra" "mathcomp-algebra-tactics" "mathcomp-analysis" - "mathcomp-boot" - "mathcomp-bigenough" - "mathcomp-character" "mathcomp-classical" - "mathcomp-field" - "mathcomp-fingroup" - "mathcomp-finmap" - "mathcomp-order" "mathcomp-reals" - "mathcomp-solvable" - "mathcomp-ssreflect" "mathcomp-zify" "math-classes" "MenhirLib" @@ -235,7 +240,9 @@ with builtins; with (import {}).lib; "rupicola" "VerdiRaft" ]; - coq-common-bundles = listToAttrs (forEach master (p: + coq-common-bundles = listToAttrs (forEach rocq-master (p: + { name = p; value.override.version = "master"; })) + // listToAttrs (forEach master (p: { name = p; value.override.version = "master"; })) // listToAttrs (forEach coq-master (p: { name = p; value.override.version = "coq-master"; })) @@ -243,18 +250,25 @@ with builtins; with (import {}).lib; { name = p; value.override.version = "main"; })) // { coq-elpi.override.version = "master"; - coq-elpi.override.elpi-version = "3.4.2"; + coq-elpi.override.elpi-version = "3.6.1"; tlc.override.version = "master-for-coq-ci"; smtcoq-trakt.override.version = "with-trakt-coq-master"; coq-tools.override.version = "proux01:coq_19955"; stdlib-refman-html.job = true; iris-examples.job = false; # Currently broken jasmin.job = false; # Currently broken, c.f., https://github.com/rocq-prover/rocq/pull/20589 + ceres-bs.job = false; # not in Rocq CI + ConCert.job = false; # not in Rocq CI ElmExtraction.job = false; # not in Rocq CI RustExtraction.job = false; # not in Rocq CI interval.job = false; # not in Rocq CI parseque.job = false; # not in Rocq CI LibHyps.job = false; # not in Rocq CI + TypedExtraction.job = false; # not in Rocq CI + TypedExtraction-common.job = false; # not in Rocq CI + TypedExtraction-elm.job = false; # not in Rocq CI + TypedExtraction-plugin.job = false; # not in Rocq CI + TypedExtraction-rust.job = false; # not in Rocq CI # To add a simple overlay applying to all bundles, # add, just below this comment, a line like #.override.version = ":"; @@ -268,13 +282,8 @@ with builtins; with (import {}).lib; trakt.job = false; # temporarily disactivated in Rocq CI smtcoq-trakt.job = false; # temporarily disactivated in Rocq CI }; - common-bundles = { - bignums.override.version = "master"; - rocq-elpi.override.version = "master"; - rocq-elpi.override.elpi-version = "3.4.2"; - rocq-elpi-test.override.version = "master"; - hierarchy-builder.override.version = "master"; - }; + common-bundles = listToAttrs (forEach rocq-master (p: + { name = p; value.override.version = "master"; })); in { "rocq-master" = { rocqPackages = common-bundles // { rocq-core.override.version = "master"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 85bfd56a5b..019107584e 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"60810ce1d3e73bece989ce9b9c42d9452c1d54a5" +"307b3a341ab73125c1c9e65603b7d6b7447539e4" diff --git a/.nix/rocq-overlays/rocq-elpi-test/default.nix b/.nix/rocq-overlays/rocq-elpi-test/default.nix index 52989d5332..57c51bc150 100644 --- a/.nix/rocq-overlays/rocq-elpi-test/default.nix +++ b/.nix/rocq-overlays/rocq-elpi-test/default.nix @@ -1,4 +1,4 @@ -{ mkRocqDerivation, rocq-elpi, stdlib, version ? null }: +{ mkRocqDerivation, rocq-core, rocq-elpi, stdlib, version ? null }: mkRocqDerivation { pname = "rocq-elpi-test"; @@ -6,7 +6,12 @@ mkRocqDerivation { owner = "LPCIC"; inherit version; - propagatedBuildInputs = [ rocq-elpi stdlib ]; + propagatedBuildInputs = [ + rocq-core.ocamlPackages.yojson + rocq-core.ocamlPackages.xml-light + rocq-elpi + stdlib + ]; useDune = true;