aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge branch 'fixminimization' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\
* | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
| | | | | | | | | | | | This makes [refine] typecheck the term only once (instead of twice), (Qed excluded of course). Fix test-suite file for output of constraints accordingly.
| * Remove no longer exported debug printerGravatar Matthieu Sozeau2016-10-21
| |
* | Merge remote-tracking branch 'github/pr/233' into v8.6Gravatar Maxime Dénès2016-10-21
|\ \ | | | | | | | | | Was PR#233: [search] Search result streaming
| | * Cleanup code according to comments.Gravatar Matthieu Sozeau2016-10-20
| | |
| | * Fix minimization to be insensitive to redundant arcs.Gravatar Matthieu Sozeau2016-10-20
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new algorithm produces different sets of arcs than in 8.5, hence existing developments may fail to pass now because they relied on the (correct but more approximate) result of minimization in 8.5 which wasn't insensitive. The algorithm works bottom-up on the (well-founded) graph to find lower levels that an upper level can be minimized to. We filter said lower levels according to the lower sets of the other levels we consider. If they appear in any of them then we don't need their constraints. Does not seem to have a huge impact on performance in HoTT, but this should be evaluated further. Adapt test-suite files accordingly.
* | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
|\ \
| * | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
| | | | | | | | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
| | * [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch converts the `search_*` functions to use an iter-style API. Consequently, the Search Vernac will produce a message for each search result, greatly improving roundtrip time as IDEs can effectively display the results in a streaming way. It also allows different printers to be used. I didn't observe a performance difference (as things seem to be dominated by printing and `Declaremods`). As a minor tweak, we make search with "Output Name Only" more efficient. Motivation: ----------- Currently, the main search API `Search.generic_search` is an effectful, iteration-based function: ```ocaml val generic_search : int option -> display_function -> unit ``` This type is imposed by `Declaremods`, which exposes an effectful, iteration-based API to traverse Coq library objects. The `Search.search_*` functions try to offer a more functional API by returning a list of pretty printing commands. They need to build an internal intermediate list for that purpose. However, this is a waste of time, as the destination of these lists is to be flushed out by the printer right away.
* | Merge remote-tracking branch 'github/printcandidates' into v8.6Gravatar Matthieu Sozeau2016-10-20
|\ \
| * | Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
|/ / | | | | | | It now prints evars with candidates as well if there are any.
* | Test for variant of #5142 (good error message on pattern-matching failure).Gravatar Hugo Herbelin2016-10-19
| |
* | Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
| | | | | | | | | | When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one.
* | More comments in VM.Gravatar Maxime Dénès2016-10-19
| |
* | Error Resiliency: more conservative default (only curly braces)Gravatar Enrico Tassi2016-10-19
| |
* | [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
| | | | | | | | | | | | | | | | | | | | PR#173 introduced a record field name clash in `stm.mli`, with duplicate fields `start/stop` for the types `focus` and `static_block_declaration`. We fix by renaming the younger ones (as to minimize code incompatibilities), but other options are possible/could be preferred, however they would be quite more invasive so I think they should be postponed for the day the Stm API is cleaned up.
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
|\ \
| * | Removing output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there.
* | | Quick fix to unification regression #4955.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The commit which caused the regression (5ea2539d4a) looks reasonable. However, it happens that this commit made that unification started in the #4955 example to follow a path with problems of the form "proj ?x == ?x" which clearly are unsolvable (both ?x have the same instance). We hack the corresponding very permissive occur-check function so that it is a bit less permissive. One day, this occur-check function would have to be rewritten in a more stricter way. ---------------------------------------------------------------------- Extra comments: I could list several functions for occur check of evars. Four of them are too strict in the sense that they do not take into account occurrences of evars which may disappear by reduction, nor evars which have instances made in such a way that the occur-check is solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are: - Termops.occur_evar for clenv, evar_refiner, tactic unification - syntactic check without any normalization, even on defined evars - Evarutil.occur_evar_upto for refine and the V82 compatibility mode - syntactic check without any normalization but inlining of defined evars - Evarsolve.occur_evar_upto_types for evar_define - syntactic check without any normalization but inlining of defined evars - occur-check in the type of evars met - optimization for not visiting several time the same evar - Evarsolve.noccur_evar for pattern unification and for inversion of substitution (evar/evar or evar/term problems) - syntactic check without any normalization but inlining of defined evars - occur-check in the type of evars met in arguments of projections - occur-check in the type of variables met in arguments of projections - optimization for not visiting several time the same evar - optimization for not visiting several time the type of the same variable - note: to go this way, it seems to me that it should check also in all types which are a cut-formula in the expression One is much too lax: - Evarconv.occur_rigidly - no recursive check except on the types of "forall" and sometimes in the arguments of an application - note: there is obviously a large room for refinements without loosing solutions
* | | Extra warning about unicode character of unknown status following an ident.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | This covers the case e.g. of "xₚ" (until the table of unicode characters is upgraded!).
* | | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | `Notation ".a" := nat.' was accepted and used for printing but not recognized in parsing. Now it does. Other examples in test-suite.
* | | Stopping warning on unrecognized unicode character in notation (fixing #5136).Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The warning was pointless since the notation was accepted and parsed anyway. We now treat unrecognized unicode characters like ordinary undefined tokens (e.g. "#" in a bare Coq). For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token" rather than "Unsupported Unicode character".
* | | [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
| | | | | | | | | | | | | | | It was not very useful as just parsing won't get you very far due to lack of notation loading.
* | | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | Given the current style in flags.mli no reason to have a function. A deeper question is why a global flag is needed, in particular the use in `interp/constrextern.ml` seems strange, the condition in the lexer should be looked at and I'm not sure about `printing/`.
* | | Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | Also renaming vernac_com into interp_vernac and eval_expr into process_vernac to clarify that it does side-effects (on the contrary of Stm.interp/Vernacentries.interp).
* | | Grouping checks about commands together.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | Moving set_formatter_out_channel where it naturally closes the corresponding opening set_formatter_output_functions.
* | | Factorizing two instances of load_vernac.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Passing chan_beautify functionally rather than by side-effect.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | This is not fully satisfactory though since we would not like to have "eval_expr" depending on a parsing/lexing/comments state... but it does because of eval_expr possibly printing the vernac expression given to it.
* | | More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8a8caba3). - Adding cLexer.current_file to the lexer state, i.e. making it a component of the type "coq_parsable" of lexer state (it was forgotten in b8ae2de5 and 8a8caba3). - Inlining save_translator/restore_translator which have now lost most of their substance.
* | | Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | It was not used any more by coqdoc since b8194b22 (Dec 2010). The table is now only part of the lexer function closure (and only in the camlp5 case).
* | | Fix compilation with camlp4 broken in 8a8caba3.Gravatar Hugo Herbelin2016-10-17
| | |
| * | Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | The fix solves the original bug report but it only turns the Not_found into a normal error in the alternative example by Guillaume. See test-suite file for comments on how to eventually improve the situation and find a solution in Guillaume's example too.
| * | Fixing a missing constraint in consider_remaining_unif_constraints.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\| |
* | | Fix output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | | | | | | | | | The output was embedding local paths from my machine.
* | | Fix previous commit.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | | | | | | | | | I've messed up with parts of the compatibility files I had to commit.
* | | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \ \
* | | | Example illustrating non-local inference of the default type of impossible ↵Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | branches (see PR #323).
| | * | Merge PR #310 into v8.5Gravatar Pierre-Marie Pédrot2016-10-17
| | |\ \
* | | \ \ Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | Test for bug #4874.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | |
* | | | | Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
| | | | |
* | | | | Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Gravatar Pierre-Marie Pédrot2016-10-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We simply explicit that the type is actually referring to the return type, not to the type of the argument of the pattern-matching. Note that the heuristic could be enhanced so as to use the same code in both let-style and match-style pattern-matching, but I'm leaving this for another time.
* | | | | Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
| | | | | | | | | | | | | | | | | | | | | | | | | When printing evar constraints, we ensure that every variable from the rel context has a name.
| | | * | Still a problem with debug auto printing.Gravatar Hugo Herbelin2016-10-15
| | | | | | | | | | | | | | | | | | | | | | | | | "msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one.
| | | * | One more little bug in the output of "debug auto".Gravatar Hugo Herbelin2016-10-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"...
* | | | | Fix bug #5139: Anomalies should not be caught by || / try.Gravatar Pierre-Marie Pédrot2016-10-14
| | | | | | | | | | | | | | | | | | | | | | | | | There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions.
| | | * | Fixing printing of info_auto broken since 0091c528 (2014).Gravatar Hugo Herbelin2016-10-14
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 07:36:42 +0000