aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | trivialGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | simplify: Environ.push_namedGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | refactoring: Names.DirPath.is_emptyGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | refactoring: Names.DirPath.compareGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | refactoring: Names.DirPath.equalGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | comment: typoGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | refactoring: Reductionops.contextual_reduction_function typeGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | Merge PR#547: [toplevel] Remove the feedback printer only on exit.Gravatar Maxime Dénès2017-04-10
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#548: [ide] Correctly place warning tags.Gravatar Maxime Dénès2017-04-10
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#460: Turning the printing primitive projection compatibility flag ↵Gravatar Maxime Dénès2017-04-09
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | off by default
| | | | | | * | | | | | | | Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use heaps instead of continuously adding elements to an ordered list, which was quadratic in the worst case. As a byproduct, this solves bug #5359, which was due to a stack overflow on big lists.
| | | | | | * | | | | | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging.
| | | | | | | * | | | | | Fast path in weak head reduction of applied atoms.Gravatar Pierre-Marie Pédrot2017-04-08
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of calling the whole reduction machirery, we check before reducing that a term is an applied atom, i.e. inductive, constructor, evar or meta. In that case, the abstract machine acts as the identity but needs to destruct and reconstruct the whole term, which can be very costly. This fixes part of bug #5421: vm_compute is very slow at doing nothing, where recomputation of the type of a big inductive was incredibly expensive.
| | | | | | | | | | * | Fixing #5460 (limitation in computing deps in pattern-matching compilation).Gravatar Hugo Herbelin2017-04-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y |- match x, y, z with ... end". But still work to do for better management of dependencies in general...
| | * | | | | | | | | | [ide] Correctly place warning tags.Gravatar Emilio Jesus Gallego Arias2017-04-08
| |/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8e07227c5853de78eaed4577eefe908fb84507c0 introduced an incorrect duplicate of `position_error_tag_at_sentence`, which sets the end of the underlining position starting at the end of the sentence, whereas the location in the feedback refers to the beginning, thus it highlights more text than it should. This was missed in 8.6 as it seems that the code was not called. We undo the duplication and fix the bug.
* | | | | | | | | | | Update the .mailmap file.Gravatar Guillaume Melquiond2017-04-08
| | | | | | | | | | |
| | | * | | | | | | | Fix a heuristic used by legacy typeclass resolution.Gravatar Pierre-Marie Pédrot2017-04-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The evarmap used by the heuristic could contain resolved evars, which could lead to a failure of backtracking in the EConstr branch. This is experimental and may be to costly.
| | | | | | | * | | | [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `process_error_hook` seems unnecesary, we just call the proper error interpretation.
| | | | | | | * | | | [stm] remove tactic_being_run hookGravatar Emilio Jesus Gallego Arias2017-04-07
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `tactic_being_run_hook` was used for the "xml" pluging but I am not sure we have a sensible use case here.
* | | | | | | | | | Merge PR#461: [camlpX] Remove camlp4 compat layer.Gravatar Maxime Dénès2017-04-07
|\ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | [toplevel] Remove the feedback feeder printing only on exit.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the bug in `Drop` reported by @mattam82: after performing a `Drop`, the feeder was lost and no further message from Coq was printed.
| | | * | | | | | | Fix an unhandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-04-07
| | | | | | | | | |
* | | | | | | | | | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Gravatar Matthieu Sozeau2017-04-07
| | | | | | | | | |
* | | | | | | | | | Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \ \ \ \ \ \ \ \
| | | | * \ \ \ \ \ \ Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| | | | |\ \ \ \ \ \ \ | |_|_|_|/ / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Remove a forgotten rule for decl_mode from the Makefile.Gravatar Pierre-Marie Pédrot2017-04-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was making the miniopt target fail.
| | | * | | | | | | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | | | | | | | | | |
| | | * | | | | | | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |_|/ / / / / / / / |/| | | | | | | | |
| | * | | | | | | | [travis] Overlay for PR#461: Camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | |
| | * | | | | | | | [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change.
| | * | | | | | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* | | | | | | | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵Gravatar Maxime Dénès2017-04-07
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | printer.
* \ \ \ \ \ \ \ \ \ Merge PR#519: Faster side effectsGravatar Maxime Dénès2017-04-07
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Inline the only use of hcons_j in Term_typing.Gravatar Pierre-Marie Pédrot2017-04-07
| | | | | | | | | | |
* | | | | | | | | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#488: Adding a documentation for the new proof engine.Gravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | Adding a documentation for the new proof engine.Gravatar Pierre-Marie Pédrot2017-04-06
|/ / / / / / / / / / / /
| | * | | | | | | | | | Documenting the fact terms are only hashconsed outside of a section.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT.
| | | | | | | | * | | | | Factor interp_instance out of Pretyping.pretype_globalGravatar Gaetan Gilbert2017-04-06
| | | | | | | | | | | | |
| | | | | | | | * | | | | Avoid strange shadowing of Pretyping.interp_universe_level_nameGravatar Gaetan Gilbert2017-04-06
| | | | | | | | | | | | |
| | | | | | | | | | | * | Fix a few programming pearls related to Time, Fail and Redirect.Gravatar Maxime Dénès2017-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis.
* | | | | | | | | | | | | Merge PR#542: [travis] Add webhook to Gitter.Gravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |
| * | | | | | | | | | | | [travis] Add webhook to Gitter.Gravatar Théo Zimmermann2017-04-06
| | | | | | | | | | | | |
| | | | | | | | | | | * | Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | | | | | | | | | | |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was needed to be done for a while.
| | | | | * | | | | | | | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
| | | | | | * | | | | | | Removing a normalization hotspot from EConstr.Gravatar Pierre-Marie Pédrot2017-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was not necessary to normalize a term just to check whether it was a global reference. The hotspot appeared in mathcomp.
| | | | | | | | | | * | | Fixing #5454 (an assert false with 'pat).Gravatar Hugo Herbelin2017-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail).
* | | | | | | | | | | | | Merge PR#434: Optimizing array mapping in the kernel.Gravatar Maxime Dénès2017-04-05
|\ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 11:56:14 +0000