aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
...
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | | | | | | | | | | | | We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
| * | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper.
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | | | | | | | | | | | | Add -o option to coqc
* \ \ \ Merge remote-tracking branch 'origin/pr/205' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \
* \ \ \ \ Merge remote-tracking branch 'origin/pr/182' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ \
| | | | | * Admitted: fix #4818 return initial stmt and univsGravatar Matthieu Sozeau2016-06-14
| | | | | |
| | * | | | STM classification: VernacTimeout may contain an "internal command".Gravatar Maxime Dénès2016-06-13
| | | | | |
| | * | | | Print Assumptions and co. can "pierce opacity".Gravatar Maxime Dénès2016-06-13
| | | | | |
* | | | | | DocumentationGravatar Enrico Tassi2016-06-07
| | | | | |
* | | | | | Renaming: ErrorBlock -> ProofBlockGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since this is really what they are. Squashing this renaming back to the root of the feature branch is hard.
* | | | | | STM: each proof block can be enabled separatelyGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | By default we enable only {} and par: that are detectable in a complete way.
* | | | | | Error box detection run only on errorGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Advantage: 0 cost if no error occurs Disadvantage: a box *must* end with the error absorbing command
* | | | | | STM: proof block detection for indentationGravatar Enrico Tassi2016-06-06
| | | | | |
* | | | | | rebase on trunkGravatar Enrico Tassi2016-06-06
| | | | | |
* | | | | | STM: fix error reporting of par:Gravatar Enrico Tassi2016-06-06
| | | | | |
* | | | | | STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
| | | | | |
* | | | | | STM: proof block detection for par:Gravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "par: tac" is a terminator, if it fails we can admit all focused goals and continue.
* | | | | | STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
| | | | | |
* | | | | | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
* | | | | | STM: carry AST and indentation of document commandsGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | This paves the way to detecting error boundaries via indentation
* | | | | | STM: support for nested boxes of nodes to model error boundariesGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Dag extended to support arbitrary clusters, renamed to Property. Vcs generalized to not impose the data hold by a Property. Stm(VCS) names a property "a box" and imposes a topological invariant (no overlap). It defines 2 kind of boxes: ProofTasks (the old cluster notion) and ErrorBound (meant to confine errors to sub-proofs). In the meanwhile more equations added to Make(..) functors in order to have just one Stateid.Set module around.
* | | | | | STM: invalid states are first class citizensGravatar Enrico Tassi2016-06-06
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A state in the cache (document node) is now one of "Empty | Error | Valid". This paves the way to commands/blocks-of-commands resilient-to/confining errors: one can catch and "ignore" the exception obtained by reaching the previous state and do something sensible, like running anyway the command or skipping until the end of an error-confining block is reached. Invalid states carry an enriched exception with the safe_id attached, so that if one edits_at or observe them gets a safe place to land (CoqIDE needs such piece of info). Little API change in Stm.state_of_id now returning a `Error variant for the new kind of state.
* | | | | Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Serialization should be specific to each particular backend, so we let the Stm clients choose how the send the nodes. This should be quite safe to pull in. Test suite passes. Related to #180
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \ \ \ | | |_|_|/ | |/| | |
| | * | | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The command line option is named: - async-proofs-delegation-threshold Values are of type float, default 1.0 (seconds). Proofs taking less that the threshold are not delegated to a worker.
* | | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * | | STM: fix argument filtering for slavesGravatar Enrico Tassi2016-05-27
| | | | | | | | | | | | | | | | | | | | Command line options to be dropped got outdated after vi -> vio renaming. This made the par: goal selector do not work in conjunction with -quick.
| * | | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible.
* | | | typosGravatar Enrico Tassi2016-05-23
| | | |
| | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
| | | | | | | | | | | | | | | | | | | | | The "Classic" string is still hard coded here in there in the system, but not in STM. BTW, the use of an hard coded "Classic" value suggests nobody really uses "Set Default Proof Mode" in .v files.
* | | STM: code cleanupGravatar Enrico Tassi2016-05-10
| | |
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
| | | | | | | | | | | | Patch by Matthieu, Enrico and myself.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\| |
| * | Build stm debugging messages lazily so that they are not silentlyGravatar Hugo Herbelin2016-04-15
| | | | | | | | | | | | | | | computed when not in debugging mode (especially those printing a command).
| * | Quick fix for #4603 (part 2): Anomaly: Universe undefinedGravatar Maxime Dénès2016-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up on Matthieu's 7e7b5684 The Definition command was classified incorrectly when a body was provided. This fix is a bit ad-hoc. A better one would require more expressiveness in side effect classification, but I'll do it in trunk only since it could impact plugins. Thanks a lot to Enrico for his help!
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ \ | | | | | | | | | | | | into JasonGross-trunk-function_scope
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |/ / | |/| |
| * | | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
| | | | | | | | | | | | | | | | | | | | Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished.
* | | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| | | |
* | | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| | | |
* | | | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
| | | |
* | | | Removing the dependency in VernacSolve in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
| | | | | | | | | | | | | | | | | | | | | | | | Instead of mangling the AST in order to interpret par: we remember the goal position to focus on it first and evaluate then the underlying vernacular expression.
* | | | Relying on Vernac classifier to flag tactics in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 11:12:40 +0000