aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-16[ci] Update fiat-crypto to the new pipelineJason Gross
We're recently reorganized fiat-crypto. This should fix the OOM CI issues. Fixes #9338
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-13Add badges linking to a selection of up-to-date Coq packages.Théo Zimmermann
The badges displaying the latest packaged version are provided by Repology. The goal is to put forward the packages that are well maintained (updated quickly after a new release) and thus recommended. The history of package updates can be found at: https://repology.org/metapackage/coq/history opam is missing because Repology is not currently tracking opam, but this could be fixed (Repology does not only track Linux-distributions-like package repositories, it also includes programming language package repositories such as CPAN, CRAN, Hackage, RubyGems, and Stackage, thus opam could be added as well).
2019-01-13Refactor badges in README.Théo Zimmermann
2019-01-11[STM] set the mtime of files generated via vio2vo (fix #9334)Enrico Tassi
2019-01-11Fix vernac classification of `Fail Instance`Maxime Dénès
AFAIK `Fail Instance` cannot open a goal.
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
Move plugin tutorial to Coq repo
2019-01-10Merge PR #9335: [STM] kill no_safe_id anomalyMaxime Dénès
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
The code to generate the legacy bodies is moved to its only user in extraction. It almost seems like we could remove it (ie no special extraction code for primitive projection constants) but then we run into issues with automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets extracted to `type foo = nat` and (if we remove the special code) `let a = a`.
2019-01-10[ci] compile with -quick & validate after vio2voEnrico Tassi
2019-01-10[vio] free resources (file descriptors) as soon as a worker endsEnrico Tassi
2019-01-10[make] support for QUICKEnrico Tassi
The variable QUICK enables the quick compilation chain: - all v files are compiled with -quick to vio files (also -native-compiler no, since it is quicker) - then all vio files are turned to vo files $NJOBS at a time All occurrences of .vo use now .$(VO) that can be either .vo or .vio depending of QUICK being defined. Targets that only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
2019-01-10[STM] kill no_safe_id anomalyEnrico Tassi
2019-01-10Merge PR #9143: Documenting the internal role of to_string and print in NamesMaxime Dénès
2019-01-10Merge PR #9331: [STM] Fix semantics of `cur_id` w.r.t. error statesEnrico Tassi
2019-01-10[checker] avoid some printing in non verbose modeEnrico Tassi
2019-01-09[STM] Fix semantics of `cur_id` w.r.t. error statesMaxime Dénès
2019-01-09Merge PR #9318: Add Azure Pipelines build badgeThéo Zimmermann
2019-01-09Merge PR #9327: [Manual] Remove link to non-existing CSS fileClément Pit-Claudel
2019-01-09Merge PR #9088: Add CI job running test suite with `async-proofs on`Emilio Jesus Gallego Arias
2019-01-09[Manual] Remove link to non-existing CSS fileVincent Laporte
2019-01-09Merge PR #9322: [ci] Update fiat-crypto legacyGaëtan Gilbert
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
[About] still says it. Close #9056.
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-09Test ltacprof in sequential modeMaxime Dénès
Scripting these commands in async mode does not really make sense.
2019-01-09Add a CI job running test suite with `-async-proofs on`Maxime Dénès
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-09Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable outputEnrico Tassi
2019-01-09Merge PR #9273: Fix #9272: `Unset Nested Proofs Allowed` does not capture ↵Enrico Tassi
nested `Ins…
2019-01-08Move position and update GitLab alt textKayla Ngan
2019-01-08[ci] Update fiat-crypto legacyJason Gross
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the master branch will no longer contain the files nor the targets for fiat-crypto legacy. (We should perhaps consider moving fiat-crypto legacy to coq-community as a source of vm and printing tests.)
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵Maxime Dénès
proofs. We forbid commands that may open proofs inside proofs.
2019-01-08Add Azure Pipelines build badgeKayla Ngan
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-08plugin_tutorial: ignore Coqlib.find_reference deprecation warning.Gaëtan Gilbert
Not sure what the right solution is here, but we can improve after the merge.
2019-01-08Fix undefined variables in coq_makefileGaëtan Gilbert
Detected by running plugin_tutorial from the main makefile which has --warn-undefined-variables on.
2019-01-08Add 'doc/plugin_tutorial/' from commit ↵Gaëtan Gilbert
'168a13dab1c9987f592994150997e692d4d7e40b' git-subtree-dir: doc/plugin_tutorial git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7 git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
2019-01-08Add doc for auto-template warningGaëtan Gilbert
2019-01-08merge-pr: add reviewer info to commit messageGaëtan Gilbert
This produces a commit message like ~~~ Merge PR #9250: coqchk: fix check for kelim with functors Reviewed-by: ppedrot Ack-by: mattam92 ~~~
2019-01-08Merge PR #9282: [ssrmatching] update license banner (fix #9281)Maxime Dénès
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation ↵Emilio Jesus Gallego Arias
of the "in" clause of a "match"
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-07Merge PR #8373: Fixes #8369: Not_found in printing message about an ↵Matthieu Sozeau
unresolved subevar.
2019-01-07Merge pull request #22 from SkySkimmer/unlicenseGaëtan Gilbert
Relicense to Unlicense
2019-01-07Merge PR #9309: [ci] Add Verdi Raft with dependencies to CIEmilio Jesus Gallego Arias
2019-01-06Merge PR #9305: Remove formal-topology from CIGaëtan Gilbert
2019-01-06Merge PR #8977: Update .mailmap.Gaëtan Gilbert
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".
2019-01-06Documenting the internal role of to_string and print in Names.Hugo Herbelin
In passing, slightly unify the API to make it clearer.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 16:52:53 +0000