aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
| | | | | | This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
* Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
|
* Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
|
* Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
| | | | | - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
* Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
| | | | | | No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely)
* Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Gravatar Pierre Letouzey2017-02-07
| | | | | | Not_found) This clarifies the execution flow
* configure: avoid deprecated warningsGravatar Pierre Letouzey2017-02-07
|
* Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
* Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileGravatar Maxime Dénès2017-02-07
|\
| * [travis] [External CI] [geocoq] don't build slow fileGravatar Emilio Jesus Gallego Arias2017-02-07
| | | | | | | | | | Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case.
* | Merge PR#424: [travis] [External CI] iris-coq: fix dependenciesGravatar Maxime Dénès2017-02-07
|\ \
| * | [travis] [External CI] iris-coq: fix dependenciesGravatar Emilio Jesus Gallego Arias2017-02-07
|/ /
* | Merge PR#421: [travis] Perform parallel testingGravatar Maxime Dénès2017-02-07
|\|
| * [travis] [External CI] GeoCoqGravatar Emilio Jesus Gallego Arias2017-02-07
| |
| * [travis] Enable 32bit test-suite + validate.Gravatar Emilio Jesus Gallego Arias2017-02-07
| |
| * [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07
| |
| * [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc ↵Gravatar Emilio Jesus Gallego Arias2017-02-07
| | | | | | | | | | | | iris-coq math-classes sf - [TLC] [metacoq] not ready for 8.6 yet
| * [travis] [External CI] Script renaming.Gravatar Emilio Jesus Gallego Arias2017-02-07
| |
| * [travis] Improvements to main scriptGravatar Emilio Jesus Gallego Arias2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Add README.ci Suggestions and comments welcome. - Use the system compiler to get some boot speedup. - Build log folding. - Set NJOBS=2 (very moderate speedup) - Set language to a defined value. OPAM itself recommends C, so we follow suit. - Remove spurious `.opam`test No harm in testing we are in the right opam setting even if the cache did exist. Anyways, it seems that the previous was spurious, as it was testing if ~/coq/.opam did exists. I think the correct command would have been: ```shell [ -e ${HOME}/.opam ] || opam init ... ``` See the log at https://travis-ci.org/coq/coq/builds/198948812 for an example.
| * [travis] [External CI] compcert HoTT math-compGravatar Emilio Jesus Gallego Arias2017-02-07
| | | | | | | | | | | | - Improve the setup to support external contribs. We use a more minimalistic Coq build, gaining a few extra minutes. - [math-comp] workaround `make -j` bug to enable parallel building.
| * [travis] Run tests using a parallel matrix.Gravatar Emilio Jesus Gallego Arias2017-02-06
|/ | | | We also optimize `travis_wait` use.
* Merge PR#419: [travis] CoqIde + doc + last available LSTGravatar Maxime Dénès2017-02-06
|\
| * [travis] : more apt deps + parallel jobs + non-container basedGravatar Pierre-Yves Strub2017-02-04
| |
| * [travis] CoqIde + doc + last available LSTGravatar Pierre-Yves Strub2017-02-04
|/
* Merge PR#418: Travis CI configurationGravatar Maxime Dénès2017-02-03
|\ | | | | | | Commits were squashed.
| * Travis CI configuration. Runs validate & test-suite.Gravatar Pierre-Yves Strub2017-02-03
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
| |\
| | * Fixing #5311 (anomaly on unexpected intro pattern).Gravatar Hugo Herbelin2017-01-31
| | | | | | | | | | | | | | | This was introduced in 8.5 while reorganizing the structure of intro-patterns.
| | * Merge PR#408: [native comp] Improve error message on linking error.Gravatar Maxime Dénès2017-01-30
| | |\
| * | | Fix a typo in STM universe communications.Gravatar Maxime Dénès2017-01-30
| | | |
* | | | Merge PR#355: Remove unused feedback_content: GoalsGravatar Maxime Dénès2017-01-30
|\ \ \ \
| | * | | Fix bug #5262: Error should tell me which name is duplicated.Gravatar Pierre-Marie Pédrot2017-01-28
| | | | |
| | * | | Fix documentation typos.Gravatar Guillaume Melquiond2017-01-27
| | | | |
* | | | | Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a modest contribution serving before all the purpose of displaying the focus stack and the shelf and give_up list. It does not print the sigma (while it could). Any improvements are welcome.
| | | | * [native comp] Improve error message on linking error.Gravatar Emilio Jesus Gallego Arias2017-01-26
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The native compiler doesn't support `Require` inside `Module` sections in some cases, we improve the error message. See: https://coq.inria.fr/bugs/show_bug.cgi?id=4335 This patch improves the error message and gives the user some feedback.
| | * | Fixing #5326 (anomaly on some unsupported case of 'pat).Gravatar Hugo Herbelin2017-01-26
| | | | | | | | | | | | | | | | | | | | We complete the support of 'pat in this particular case (a 'pat under a binder in a notation).
| | * | Merge PR#383: fix #5244: set printing width ignored when given enough spaceGravatar Maxime Dénès2017-01-24
| | |\ \
| | * \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| | |\ \ \ | | | | |/ | | | |/|
| | | * | Fixing unification regression #5323.Gravatar Hugo Herbelin2017-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Tracking conversion problems to reconsider was lost for evars subject to restriction (field last_mods was not updated and conversion problems not considered to be changed).
* | | | | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case.
| | * | | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing a matching over a "catch-all" variable, when let-ins occur in the arity. However ade2363e35 failed to understand what was the correct fix, introducing instead the regressions mentioned in #5322 and #5324. This fixes all of #5322 and #5324, as well as the handling of let-ins in the arity. Thanks to Jason for helping in diagnosing the problem.
| | * | | Revert "Process Next Obligation proofs in parallel (fix #5314)"Gravatar Enrico Tassi2017-01-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070. It seems the proof terminator of obligation.ml, in the case in which Set Shrink Obligation is set, accesses the opaque proof.
| | * | | Process Next Obligation proofs in parallel (fix #5314)Gravatar Enrico Tassi2017-01-20
| | | | |
| | * | | Do not add redundant side effects in tactic code.Gravatar Pierre-Marie Pédrot2017-01-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was observable in long proofs, because side effects kept being duplicated, leading to an additional cost linear in the size of the proof. This commit touches kernel files, but the corresponding API is only used in tactic-facing code so that the side_effects type remains opaque. Thus it does not affect the kernel safety.
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Mapping named_context_val preserves sharing when possible.Gravatar Pierre-Marie Pédrot2017-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was deactivated by 27c9346 and made an optimization moot in eauto. This optimization was physically checking for equality, but as lists where rebuilt by the mapping, this was never true. Some contribs were thus quite slower, including persistent-union-find which was twice slower. This 2-line patch fixes it by trying to preserve sharing as much as possible. Note that we should still do something about eauto, because it does redo useless work a lot whenever the environment only changes a bit, while we could cache this computation.
| * | | | STM: fix run-time classification of VernacInstance (fix #5313)Gravatar Enrico Tassi2017-01-17
| | | | |
| * | | | Fixing (part of) #5303 (clarifications around Record/Structure/Variant).Gravatar Hugo Herbelin2017-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - We fix the inconsistency of Structure and Record which according to doc are the same. - We improve the error message when not using { ... } for Record or Structure.
| * | | | Fix race condition in STM DAG generation (in debug mode).Gravatar Maxime Dénès2017-01-13
| | | | | | | | | | | | | | | | | | | | The same file name for .dot graphs could be used by concurrent processes.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:41:23 +0000