aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* 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.
* typosGravatar Enrico Tassi2016-05-23
|
* 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
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\| |
| * | Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Gravatar Pierre-Marie Pédrot2016-03-15
| | | | | | | | | | | | | | | | | | | | | | | | The SIGINT sent to the master coqtop process was lost in a watchdog thread, so that the STM resulted in an inconsistent state. This patch catches gracefully the exception and kills the task as if it were normally cancelled. Note that it probably won't work on non-POSIX architectures, but it does not really matter because interrupt was already badly handled anyway.
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
| | | | | | | | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\| |
| * | STM: Print/Extraction have to be skipped if -quickGravatar Enrico Tassi2016-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull.
| * | STM: classify some variants of Instance as regular `Fork nodes.Gravatar Enrico Tassi2016-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "Instance name : Type." is like "Lemma name : Type", i.e. it starts a proof. Unfortunately sometimes it does not, so we say VtUnknown. Still, if there is an open proof, we classify it as a regular Lemma, i.e. the opacity depends only on the terminator. This makes CoqIDE and PIDE based UI way more responsive when processing files containing Instance that are proved by tactics, since they are now correctly delegated to workers. Bug reported privately by Alec Faithfull.
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ | | |/ / | |/| |
| * | | STM: always stock in vio files the first node (state) of a proofGravatar Enrico Tassi2016-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used not to be the case when the proof contains Sideff, since the code was picking the last known state and not necessarily the first one. Because of side effects the last known state could be the one corresponding to the side effect (that was executed to, say, change the parser). This is also related to bug #4530
| * | | STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Gravatar Enrico Tassi2016-02-10
| | | |
| | * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
| * | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| | |
* | | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
| | |
* | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around.
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\| |
| * | fixup d2b468a, evar normalization is neededGravatar Enrico Tassi2016-01-04
| | |
| * | par: check if the goal is not ground and fail (fix #4465)Gravatar Enrico Tassi2016-01-04
| | |
| * | workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
| | |
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
| | | | | | | | | | | | | | | Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* | | Remove some useless module opening.Gravatar Guillaume Melquiond2016-01-02
| | |
* | | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
| | |
* | | Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
| | |
* | | Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
| | |
* | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
| | |
* | | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that.
* | | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular ↵Gravatar Matej Kosik2015-12-18
| | | | | | | | | | | | command is mapped.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 11:33:39 +0000