| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-05 | Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12) | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-03-03 | [build] Split stdlib to it's own opam package. | Emilio Jesus Gallego Arias | |
| We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine. | |||
| 2021-02-27 | Add overlay | Pierre Roux | |
| 2021-02-26 | Expose Top_printers.econstr_display | Gaëtan Gilbert | |
| 2021-02-24 | Overlay for Set Debug | Gaëtan Gilbert | |
| 2021-02-22 | Fix the release process checklist with respect to the refman update. | Théo Zimmermann | |
| 2021-02-17 | Add an entry to file critical-bugs. | Guillaume Melquiond | |
| 2021-02-11 | Merge 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 elpi | Enrico Tassi | |
| 2021-02-11 | Merge 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 function | Enrico Tassi | |
| 2021-02-11 | Merge PR #13847: [ci] elpi 1.13.0 | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-02-11 | overlay for coq-elpi | Enrico Tassi | |
| 2021-02-11 | [ci] elpi 1.13.0 | Enrico Tassi | |
| 2021-02-10 | Merge PR #13818: [bench] Re-enable coq-performance-tests | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-02-04 | Update release process following coq/ceps#52. | Théo Zimmermann | |
| 2021-02-04 | Merge PR #13528: [RM] Script to list the contributors between two git revisions | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Reviewed-by: gares | |||
| 2021-02-04 | Use release branch instead of master. | Théo Zimmermann | |
| 2021-02-03 | [bench] Re-enable coq-performance-tests | Jason 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-02 | Add VST to the set of default bench packages. | Pierre-Marie Pédrot | |
| 2021-02-02 | Merge PR #13805: Bench: remove broken packages | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-02-02 | Bench: don't uselessly rely on initialized opam | Gaëtan Gilbert | |
| AFAICT this init.sh call is useless. | |||
| 2021-01-29 | Bench: remove broken packages | Gaë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-27 | Add sysinit to load_printer lists | Gaëtan Gilbert | |
| 2021-01-27 | [sysinit] new component for system initialization | Enrico 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-21 | Add missing item about PDF manual to release checklist. | Théo Zimmermann | |
| 2021-01-19 | Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵ | Pierre-Marie Pédrot | |
| pattern Reviewed-by: ppedrot | |||
| 2021-01-18 | Adding overlay for perennial. | Hugo Herbelin | |
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2021-01-13 | Merge PR #13740: [osx] macpack also coqidetop (for libgmp) | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2021-01-13 | Merge PR #13598: [ci] window jobs based on the platform | Michael Soegtrop | |
| Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-12 | [osx] macpack all binaries, not just coqide | Enrico Tassi | |
| 2021-01-12 | Merge PR #13704: [ci] [coq-performance-tests] Errors at end of log | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: gares | |||
| 2021-01-11 | [ci] [coq-performance-tests] Errors at end of log | Jason 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-09 | Merge PR #13299: Remember universe instances of constants in notations | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2021-01-07 | Merge PR #13718: Move printing and sorting out of AcyclicGraph | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-06 | Further 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 platform | Enrico Tassi | |
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
| 2021-01-04 | Document the change of case representation. | Pierre-Marie Pédrot | |
| 2021-01-04 | Add overlays. | Pierre-Marie Pédrot | |
| 2021-01-04 | Change 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-04 | Merge 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 ones | Enrico Tassi | |
| 2021-01-01 | Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-30 | Merge PR #13692: Fix failing Windows CI builds. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-30 | Merge PR #13321: Move evaluable_global_reference from Names to Tacred. | coqbot-app[bot] | |
| Reviewed-by: herbelin Ack-by: ejgallego | |||
| 2020-12-30 | Fix 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-28 | Register a printer for fconstr substitutions in the kernel. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |