aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
|
* TQueue: new primitive to take a snapshot of the queueGravatar Enrico Tassi2014-10-13
|
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
| | | | | Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof.
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
| | | | | | | | | | | | | | Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
|
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
| | | | It is not 100% complete, but the main part is there.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* Marshalling errors should be bold and red (should never happen actually)Gravatar Enrico Tassi2014-09-09
|
* A marshalling failure does not make a worker `OldGravatar Enrico Tassi2014-09-09
|
* Back: print subgoals as in 8.4 (Close: 3585)Gravatar Enrico Tassi2014-09-09
|
* BackTo not part of the doc when used by emacsGravatar Enrico Tassi2014-09-09
| | | | Used to work "by chance".
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
|
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
|
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* stm: use xlabel insted of label in dot (debug) outputGravatar Enrico Tassi2014-09-02
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
| | | | stm test-suite files.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* STM: Classify Let as non asynchronous (Closes: #3486)Gravatar Enrico Tassi2014-08-05
|
* STM: when looking up in the cache catch Expired excGravatar Carst Tankink2014-08-04
|
* STM: generate Feedback message for parsing errorsGravatar Enrico Tassi2014-08-04
|
* STM: use a real priority queueGravatar Enrico Tassi2014-08-04
|
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
|
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
|
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
|
* STM: check-vi-task fixedGravatar Enrico Tassi2014-07-16
|
* STM: Goal printing got wrong in a merge, fixedGravatar Enrico Tassi2014-07-16
|
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
|
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
| | | | This is useful if a UI does not support that
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
|
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
|
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
| | | | | LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
|
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
|
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
| | | | These are now sufficient to implement PIDE
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
|
* Typo in stm error message.Gravatar Hugo Herbelin2014-06-28
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively.
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
| | | | Every time you use abstract a kitten dies, please stop.
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
| | | | | | and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-04 07:36:36 +0000