aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2021-02-24Overlay for Set DebugGaëtan Gilbert
2021-02-22Fix the release process checklist with respect to the refman update.Théo Zimmermann
2021-02-17Add an entry to file critical-bugs.Guillaume Melquiond
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵coqbot-app[bot]
function Reviewed-by: ejgallego
2021-02-11[ci] overlay for elpiEnrico Tassi
2021-02-11Merge PR #13823: Update release process following coq/ceps#52.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: gares
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-11Merge PR #13847: [ci] elpi 1.13.0coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-11overlay for coq-elpiEnrico Tassi
2021-02-11[ci] elpi 1.13.0Enrico Tassi
2021-02-10Merge PR #13818: [bench] Re-enable coq-performance-testscoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-04Update release process following coq/ceps#52.Théo Zimmermann
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-03[bench] Re-enable coq-performance-testsJason Gross
Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04. coq-performance-tests was fixed in https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1. Note that the current state is not optimal, as the bench does not test the native compiler at all (see #13807).
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:17 +0000