aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
* Delay use of flag "Discriminate Introduction" from interp to execution time.Gravatar Hugo Herbelin2017-10-26
|
* Merge PR #5989: Handle ∞ in coq-makefile timing test-suiteGravatar Maxime Dénès2017-10-20
|\
* \ Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵Gravatar Maxime Dénès2017-10-20
|\ \ | | | | | | | | | just Iris
* \ \ Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974).Gravatar Maxime Dénès2017-10-20
|\ \ \
* \ \ \ Merge PR #5972: Fixing link to GitHub issue search, and wording.Gravatar Maxime Dénès2017-10-20
|\ \ \ \
* \ \ \ \ Merge PR #1155: Use type nonrec in some functor arguments.Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1147: Remove GeoProof support.Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | clause of an inductive definitions
* \ \ \ \ \ \ \ Merge PR #1095: [stm] Remove state handling from FuturesGravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #960: Uniformize references to BugzillaGravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \
| | | | | | | | * | rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
| | | | | | | | | |
| | | | | | | | | * Handle ∞ in coq-makefile timing test-suiteGravatar Jason Gross2017-10-19
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | This should (hopefully) fix #5675.
| * | | | | | | | Moving bug numbers to BZ# format in the CHANGES file.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers.
| * | | | | | | | Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
| * | | | | | | | Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
| | | | | | | * CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
| |_|_|_|_|_|/ |/| | | | | |
| | | | | | * Bugzilla autolink: avoid linking inside links (fix #5974).Gravatar Gaëtan Gilbert2017-10-18
| |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #984: Handling primitive projections in canonical structures.Gravatar Maxime Dénès2017-10-18
|\ \ \ \ \ \
| | | | | | * Fixing link to GitHub issue search, and wording.Gravatar Théo Zimmermann2017-10-18
| |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #1149: Moving to GitHub issues.Gravatar Maxime Dénès2017-10-18
|\ \ \ \ \ \
| * | | | | | Moving to GitHub issues.Gravatar Théo Zimmermann2017-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds an issue template asking for version and OS information and adapts the contributing guide to the change of bug tracker.
| | * | | | | Adding a test for bug BZ#5692.Gravatar Pierre-Marie Pédrot2017-10-17
| | | | | | |
| | * | | | | unification: fix BZ#5692, recognize prim projs as CS projectionsGravatar Matthieu Sozeau2017-10-17
| | | | | | |
| | * | | | | Properly handling projection parameters in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
| | | | | | |
| | * | | | | Handling primitive projections in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
| |/ / / / / |/| | | | |
| | * | | | [vernac] [state] Cache freeze/unfreezeGravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Users need to be careful wrt global state modification outside `Vernacentries` without registering the functions. In particular, our fail implementation also has to invalidate the cache.
| | * | | | [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
| | * | | | [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We still don't thread the state there, but this is a start of the needed infrastructure.
| | * | | | [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away.
| | * | | | [stm] First step to move interpretation of Undo commands out of the classifier.Gravatar Emilio Jesus Gallego Arias2017-10-17
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself.
* | | | | Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Maxime Dénès2017-10-16
|\ \ \ \ \
| | | | | * Use type nonrec in some functor arguments.Gravatar Gaëtan Gilbert2017-10-16
| |_|_|_|/ |/| | | |
* | | | | Merge PR #1152: Fix BZ#5785 (make install -j broken)Gravatar Maxime Dénès2017-10-16
|\ \ \ \ \
| | * | | | [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Emilio Jesus Gallego Arias2017-10-15
| |/ / / / |/| | | | | | | | | | | | | | The test suite cases are preserved until the feature is actually removed.
| * | | | Fix some more missing mkdir lines to Makefile.ideGravatar Jason Gross2017-10-13
| | | | |
| * | | | Fix BZ#5785 (make install -j broken)Gravatar Jason Gross2017-10-13
|/ / / / | | | | | | | | | | | | | | | | This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between 8.6 and 8.7.
* | | | Merge PR #1103: Take Suggest Proof Using outside the kernel.Gravatar Maxime Dénès2017-10-13
|\ \ \ \
* \ \ \ \ Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ↵Gravatar Maxime Dénès2017-10-12
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | STM (BZ#5556)
* \ \ \ \ \ Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Gravatar Maxime Dénès2017-10-12
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | | | | | | | | directory` on every execution
| | | | | * Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* | | | | Merge PR #1054: Restoring test on ident validity while browsing directory ↵Gravatar Maxime Dénès2017-10-11
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | structure.
| | * | | | Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Gravatar Maxime Dénès2017-10-11
| | | | | | | | | | | | | | | | | | | | | | | | execution
| | | * | | [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move delicate library/module instillation code to the STM so the API guarantees that the first state snapshot is correct. That was not the case in the past, which meant that the STM cache was unsound in batch mode, however we never used its contents due to not backtracking to the first state. This provides quite an improvement in the API, however more work is needed until the codepath is fully polished. This is a critical step towards handling the STM functionally.
* | | | | | Merge PR #1143: fix coq_makefile on cygwinGravatar Maxime Dénès2017-10-11
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | | | * | Stm.get_hint_ctx: remove unused Str.splitGravatar Gaëtan Gilbert2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With suggest proof using out of the kernel the format of context_used in .aux is just the list of ids wanted by get_hint_ctx. (split x s when x doesn't appear in s just returns the singleton list [s])
| | | | * | Parse [Proof using Type] without translating Type to an id.Gravatar Gaëtan Gilbert2017-10-10
| | | | | |
| | | | * | Use a nice printer for constant names in Suggest Proof Using.Gravatar Gaëtan Gilbert2017-10-10
| | | | | |
| | | | * | Code factorization Vernacentries.interp on VernacProof.Gravatar Gaëtan Gilbert2017-10-10
| | | | | |
| | | | * | [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:05:06 +0000