aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2021-02-04Merge PR #13528: [RM] Script to list the contributors between two git revisionscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2021-02-04Use release branch instead of master.Théo Zimmermann
2021-02-02Add VST to the set of default bench packages.Pierre-Marie Pédrot
2021-02-02Merge PR #13805: Bench: remove broken packagesPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-02Bench: don't uselessly rely on initialized opamGaëtan Gilbert
AFAICT this init.sh call is useless.
2021-01-29Bench: remove broken packagesGaëtan Gilbert
performance-tests and sf-plf have been failing for a long time without updates, there's no point wasting time partally building them.
2021-01-27Add sysinit to load_printer listsGaëtan Gilbert
2021-01-27[sysinit] new component for system initializationEnrico Tassi
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
2021-01-21Add missing item about PDF manual to release checklist.Théo Zimmermann
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-18Adding overlay for perennial.Hugo Herbelin
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-13Merge PR #13740: [osx] macpack also coqidetop (for libgmp)Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-01-13Merge PR #13598: [ci] window jobs based on the platformMichael Soegtrop
Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-12[osx] macpack all binaries, not just coqideEnrico Tassi
2021-01-12Merge PR #13704: [ci] [coq-performance-tests] Errors at end of logcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares
2021-01-11[ci] [coq-performance-tests] Errors at end of logJason Gross
By running `make -k; make` whenever `make` initially fails, we can get error messages to occur at the end of the log. This way they'll show up on the GitHub Actions preview/summary, rather than me having to go digging for them in the GitLab logs.
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
We expose the representation function in UGraph and change the printer signature to work over the representation instead of the abstract type. Similarly, the topological sorting algorithm is moved to Vernacentries. It is now even simpler.
2021-01-05[ci] windows job based on the platformEnrico Tassi
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Add overlays.Pierre-Marie Pédrot
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2021-01-04Merge PR #13685: Add a debug printer for fconstr substitutions.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-04[win] remove old scripts, we now use the platform onesEnrico Tassi
2021-01-01Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3.coqbot-app[bot]
Reviewed-by: gares
2020-12-30Merge PR #13692: Fix failing Windows CI builds.coqbot-app[bot]
Reviewed-by: gares
2020-12-30Merge PR #13321: Move evaluable_global_reference from Names to Tacred.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: ejgallego
2020-12-30Fix failing Windows CI builds.Théo Zimmermann
Following a recent change in Cygwin. Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2020-12-30[ci] Switch to testing the maintenance branch for Flocq 3.Théo Zimmermann
This is the version that CompCert will be compatible with for the time being.
2020-12-28Register a printer for fconstr substitutions in the kernel.Pierre-Marie Pédrot
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: palmskog
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-21Add overlays.Pierre-Marie Pédrot
2020-12-18Do not load overlay data (workaround to fix CI).Théo Zimmermann
2020-12-17[ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI.Théo Zimmermann
2020-12-16Merge PR #13644: Fix overlay system: projects need to be loaded before overlays.coqbot-app[bot]
Reviewed-by: gares
2020-12-16Merge PR #13616: Bench: add .log extension to .stdout/stderr filesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
Also fixes is_in_projects
2020-12-15Merge PR #13615: Document the manual tasks that I need to do at each release.coqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13633: [ci] uniform name of projects w.r.t. opam packagescoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-15Merge PR #13632: [ci] Update pin ci scriptcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-15[ci] uniform name of projects w.r.t. opam packagesEnrico Tassi
This makes it easier to track projects across Coq's CI and the platform
2020-12-14Update dev/tools/pin-ci.shEnrico Tassi
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-12-14[ci] simplify script to pin ci projectsEnrico Tassi
2020-12-14[ci] fix code to check if the overlay is validEnrico Tassi
2020-12-13Update dev/ci/user-overlays/README.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-12[ci] update doc for overlaysEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:08:15 +0000