coq/ide/coqide/protocol, branch master The formal proof system [build] Split stdlib to it's own opam package. 2021-03-03T15:06:14+00:00 Emilio Jesus Gallego Arias 2020-06-22T15:52:18+00:00 ab98d847d237af3cd0e46edef42218be65cfc98f 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. 
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.
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol 2020-10-12T16:34:24+00:00 coqbot-app[bot] 2020-10-12T16:34:24+00:00 2ff70d8341177d384043dd3d02da6968a8788e32 Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego 
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
Add an XML message for "Show Proof Diffs" 2020-10-10T02:25:25+00:00 Jim Fehrle 2020-08-23T23:09:10+00:00 1d4bbefe5fe19306ab415e537863763a0a74134a Add menu item that uses this 
Add menu item that uses this
Dropping the misleading int argument of Pp.h. 2020-10-08T21:47:14+00:00 Hugo Herbelin 2020-10-05T20:21:04+00:00 db278921c54201a01543953cc0986fc0fb126615 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. 
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.
Add a check of empty list of arguments in xmlprotocol where relevant. 2020-10-08T21:46:29+00:00 Hugo Herbelin 2020-10-05T20:12:57+00:00 e18ed350f7b5710c382ea1306e7b1e7e2fb0c9f8 






Move CoqIDE to its own folder
2020-06-02T16:53:33+00:00

Maxime Dénès

2020-05-16T15:07:37+00:00

33021618a06a94563d28691940f02a55bd9d358d

The will make it possible to put a VsCoq toplevel in `ide/vscoq`.





The will make it possible to put a VsCoq toplevel in `ide/vscoq`.