aboutsummaryrefslogtreecommitdiff
path: root/ide/coqide
AgeCommit message (Collapse)Author
2021-04-19Merge PR #14068: [build] Remove leftovers of code signing / OSX IDE ↵coqbot-app[bot]
infrastructure Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-04-19Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be ↵Pierre-Marie Pédrot
set/unset as a modifier Reviewed-by: ppedrot
2021-04-19[build] Remove leftovers of codesigning / OSX IDe infrastructure.Emilio Jesus Gallego Arias
This is not used anymore, and after #14122 the makefile parts for the dmg generation are not used anymore. Closes #7476 .
2021-04-18Coqide: on MacOS X, allow the command key to be set/unset as a modifier.Hugo Herbelin
This is done by: - allowing the <Meta> gtk modifier (gtk internal name for Command) to be used as a modifier by default on MacOS X - printing it <cmd> in the preference window when on MacOS X
2021-04-12Merge PR #14046: make critical sections safe in the presence of exceptionscoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: gares Ack-by: SkySkimmer Ack-by: gadmm
2021-04-09Make critical sections safe in the presence of exceptionsLasse Blaauwbroek
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion. This ensures that exceptions thrown by signals will not leave the system in a deadlocked state.
2021-04-08Fix a GTK warning in CoqIDE introduced by #14063.Pierre-Marie Pédrot
The Variant entry was appearing twice, leading to a duplicate warning.
2021-04-08Merge PR #14062: Fixes #11690: wrongly toggled coqide printing matching flagPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
From an OCaml library point of view.
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02Fixes #10720: highlighting Variant in CoqIDE.Hugo Herbelin
2021-04-02Fixes #11690: wrongly toggled coqide printing matching flag; moving raw->nested.Hugo Herbelin
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make ↵coqbot-app[bot]
them more stable. Reviewed-by: SkySkimmer Reviewed-by: gares
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-17Add option --version to Coqide (fix #13752).Guillaume Melquiond
2021-02-16Get rid of the compilation date from the binaries to make them more stable.Guillaume Melquiond
Contrarily to the comments, Coq_config.date was not the "release date" but just another "compile date".
2021-02-02ide: lablgtk fixesslrnsc
2021-02-01ide: shift+enter to find backwardsslrnsc
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-27[coqtop] handle -print-module-uid after initializationEnrico Tassi
2021-01-27[sysinit] move initialization code from coqtop to hereEnrico Tassi
We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits.
2021-01-27[sysinit] new component for system initializationEnrico Tassi
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2020-12-18Fixes #13657: vscoq needs goal uid.Hugo Herbelin
2020-10-30Adding support for printing goal names in CoqIDE.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-08Add a check of empty list of arguments in xmlprotocol where relevant.Hugo Herbelin
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-01Unify the shelvesMaxime Dénès
Before this patch, the proof engine had three notions of shelves: - A local shelf in `proofview` - A global shelf in `Proof.t` - A future shelf in `evar_map` This has lead to a lot of confusion and limitations or bugs, because some components have only a partial view of the shelf: the pretyper can see only the future shelf, tactics can see only the local and future shelves. In particular, this refactoring is needed for #7825. The solution we choose is to move shelf information to the evar map, as a shelf stack (for nested `unshelve` tacticals). Closes #8770. Closes #6292. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-06Repair coqide option "Display parentheses"Jean-Christophe Léchenet
2020-06-29Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
This is in preparation for the next commit which will clean-up the current API flow in `Declare`.
2020-06-23CoqIDE: fix lexing of UTF-8 in quotations like constr:()James Lottes
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-02Move CoqIDE to its own folderMaxime Dénès
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:54 +0000