aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Collapse)AuthorAge
* Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
| | | | | | Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\
| * Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Gravatar Maxime Dénès2015-11-02
| |
| * STM: fix undo into a branch containing side effectsGravatar Enrico Tassi2015-11-02
| | | | | | | | The "master" label used to be reset to the wrong id
| * STM: never reopen a branch containing side effectsGravatar Enrico Tassi2015-11-02
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
| | | | | | | | involving Futures.
| * Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
| | | | | | | | universes are declared correctly in the enclosing proofs evar_map's.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
| | | | | | | | | | The splines=ortho option seems to make dot crash sometimes, so this commit removes it from the STM debugging output
| * STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
| | | | | | | | PIDEtop needs these to implement its new transaction mechanism
| * STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
| | | | | | | | | | This lets hooks treat different exceptions in different ways; in particular, user interrupts can now be safely ignored
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | | | | | | | | | | | | | | - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems.
| * STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
| |
| * STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
| |
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
|/ | | | | | The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap.
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
| | | | | ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel.
* STM: save a full state for queries.Gravatar Enrico Tassi2015-09-01
| | | | | | | | | | | In PIDE based UIs queries can be delegated too, hence to speed up things I was saving a shallow state. Unfortunately a shallow state breaks section/modules commands, and a query can be the last entry of a section/module. (A shallow state does essentially drop the libstack). The easy solution is to save a complete state. A better one would be to refine the static analysis of the document and decide which kind of saved state one needs.
* STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
|
* STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
|
* STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
|
* STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
|
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
|
* ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)Gravatar Enrico Tassi2015-07-28
|
* STM: fix a "exn with no safe id attached" error on a failing queryGravatar Enrico Tassi2015-07-14
| | | | It showed up at the CoqCS.
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
| | | | Hence we reuse the ones in master.
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
|
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
|
* nice error for Restart outside a proof (Close: #4235)Gravatar Enrico Tassi2015-05-12
|
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
| | | | | | | The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
* STM: print trace on "anomaly, no safe id attached"Gravatar Enrico Tassi2015-04-21
|
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
| | | | | | | | | | | No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch.
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
| | | | | | | | | | | | | | When a worker sends back a system state to master, it tries to just send a delta. If the command is a simple tactic, then only the proof state changes. Now, what is a simple tactic? 1. a tactic 2. that does not change the environment Check 1. was surely incomplete. Now it is: VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ Is it complete?
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
| | | | | | | | | | | | | | | | | | | | | This is likely to make nested proofs containing proof modes switch broken, but fixes the problems Arnaud has in his branch. It is possible that the classification function we have today is not fine grained enough. If a command that changes the proof mode has as the only global effect changing the proof mode, then the current code is fine. If it has a more global effect that persists after the proof is over but has no impact on the proof itself, then the old code is fine. As far as I can get, the proof mode switching commands have a global effect (changing parser) but also a proof effect (un/focusing). We don't have a classification for these. Today a command having a global effect is played twice: on the proof branch an on master. Of course if such command cannot work on master (where there is no finished proof for example) we need a special treatment for it.
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
|
* STM: if Set Universe Polymorphism then synchronous (#4119)Gravatar Enrico Tassi2015-03-22
| | | | | It was detecting only the per-lemma Polymorphic flag, but not the global one.
* STM: do not delegate proofs containing PrintGravatar Enrico Tassi2015-03-22
|
* STM: after every command restore the expected proof modeGravatar Enrico Tassi2015-03-22
|
* Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Gravatar Pierre Courtieu2015-03-20
| | | | | | | | | | | | | | | | | In PG there are shortcuts that perform on the fly "Set Printing All"/"Unset Printing All" in pg. For example if you type C-u before some shortcut for print (check/About/Show), it performs: Set Printing All. Print foo. Unset Printing All. But if the "Unset" prints a goal, then pg interprets the output of Print as a command applied on a previous line, and thus hides it. So for emacs mode I would prefer no goal printing when options are set/unset. In the situation where this should be done (when setting durably the option probably), I'd rather program a "Show" explicitely.
* STM: -debug: better explanation of why not async (#4125)Gravatar Enrico Tassi2015-03-15
|
* STM: -quick: async no Proof using but no Section (#4124)Gravatar Enrico Tassi2015-03-15
| | | | As happens in interactive mode.
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
|
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
|
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
| | | | | Workers send back incomplete system states (only the proof part). Such part must include the meta/evar counter.
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
|
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
| | | | This change fixes performance problems in PIDE based user interfaces
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-06 03:42:50 +0000