aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* STM: make ~valid state id non optional from APIsGravatar Enrico Tassi2016-10-26
| | | | | | It used to be Stateid.initial by default. That is indeed a valid state id but very likely not the very best one (that would be the tip of the document).
* [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.
* Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| | | | | | | | | | For now, the only meaningful user is "Set Warnings". Example: Section Bar. Local Set Warnings Append "-foo". (* warning foo is now disabled *) End Bar. (* foo is now reenabled, assuming it was before entering the section *)
* STM: compute the correct state for edited Qed (#5086)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | When a proof is 're-opened', the Qed node does not change. Still the STM has to install the old state (where only the future proof has to be updated). This bit was missing. Why was it working: the bug happens only if you reopen the very last proof, i.e. there is no sentence that stays valid after the Qed. If there is such a sentence, its state was computed correctly before, and is not changed. If it is the very last, then the next state is based on the wrong one...
* Cleanup API, making inference_hook optionalGravatar Matthieu Sozeau2016-09-29
|
* Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
| | | | | | This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic.
* AsyncTaskQueue: annotate debug feedback messages with worker idGravatar Enrico Tassi2016-09-13
|
* stm: feedback forwarding has to be atomicGravatar Enrico Tassi2016-09-13
| | | | | | I think that a better place for the mutex would be the printing routine, but I still hope we will get rid of threads in favor of coroutines. So I keep all mutexes in Stm.
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-07
|\
* | STM: if_verbose on "Checking task ..." (fix #4058)Gravatar Enrico Tassi2016-09-07
| |
* | STM: queries give back a dummy safe_id in case of error (#5041)Gravatar Enrico Tassi2016-09-06
| |
* | STM: sideff: report safe_id correctly (fix #4968)Gravatar Enrico Tassi2016-09-06
| |
* | STM: nested Abort is like nested Qed (fix #4756)Gravatar Enrico Tassi2016-09-06
| | | | | | | | | | | | There was an "optimization", since Abort is an empty side effect. But that optimization had an impact on the DAG shape. Now a nested proof, no matter if it is kept or dropped, is handled the same.
| * Fix #5065: Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05
| | | | | | | | | | | | Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough.
* | feedback: support multiple feedback listenersGravatar Enrico Tassi2016-09-05
| | | | | | | | So that a module can add his own and look at the traffic
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
|\|
| * Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
| | | | | | | | | | | | We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
| * Fix #4871 - interrupting par:abstract kills coqtopGravatar Maxime Dénès2016-08-30
| | | | | | | | Fix done with Enrico.
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* | Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | | | When declaring the universes of a lemma explicitely, throw an error if after minimization the type of a lemma still refers to unbound universes. This is a fix and an incompatibility, but scripts will be backwards compatible themselves. Fix another minor bug in treating universe binders for (Co)Fixpoint.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | [feedback] Remove `ErrorMsg` in favor of `Message Error`.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | | | | | | | | | | | | | The ErrorMsg datatype was introduced to allow locations in messages, however, it was redundant with error and used only in one place. We remove it in favor of a more uniform treatment of messages with location. This patch also removes the use of `Loc.ghost` in one place. Lightly tested.
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:49:00 +0000