coq/gramlib, branch master The formal proof system Relying on the abstract notion of streams with location for parsing. 2021-04-23T13:34:29+00:00 Hugo Herbelin 2021-04-05T14:40:10+00:00 e07efb3798c7c6ec54aac9093ab50fddfc6c6a5b We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml). 
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml. 2021-04-23T13:34:29+00:00 Hugo Herbelin 2021-04-05T14:24:39+00:00 52a71bf2b1260ce8f8622878c82caec54d298808 






Gramlib: token_ematch has a useless argument.
2021-04-23T13:34:29+00:00

Hugo Herbelin

2021-04-03T22:05:17+00:00

24bee7cf490bcd2564450aee4b2b09c245175a02












Gramlib: documentation of the recovery mechanism.
2021-04-08T15:35:42+00:00

Hugo Herbelin

2021-04-04T09:48:20+00:00

13d6756e02919fe366b6cbd3253f6bd331e0b9da












Gramlib: some comments about how new rules are inserted.
2021-04-08T15:35:42+00:00

Hugo Herbelin

2021-04-04T02:43:20+00:00

4c3247586a86ff528d9eee6d8a1c8266f3d3fca1












Gramlib: some comments about the main start/continue parsing loop.
2021-04-08T15:35:42+00:00

Hugo Herbelin

2020-02-12T07:06:42+00:00

8716a37faeff72a38aae5cf5b6835ceab470e95c












[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.







Add flag -open Gramlib so that merlin works in gramlib with make.
2020-10-14T19:24:52+00:00

Hugo Herbelin

2020-10-14T19:23:59+00:00

678aaa19687be94c380e34fee81a9948e3307b9d












[gramlib] Remove legacy located exception wrapper in favor of standard infrastructure.
2020-07-16T13:54:31+00:00

Emilio Jesus Gallego Arias

2020-07-15T15:33:04+00:00

4a4d35baf47944f4d30bd10de7e71f46f17da8f2

The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695





The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695







[gramlib] Don't expose unsafe interfaces to clients
2020-03-26T03:45:57+00:00

Emilio Jesus Gallego Arias

2020-03-13T11:21:27+00:00

5c9f318f5f1b6e85b03bba9450ac059377be54fc

I'd say this is more of a temporary measure than a long-term plan; IMO
we should make the interfaces safe so `Gramlib.Grammar` does provide
only one signature.





I'd say this is more of a temporary measure than a long-term plan; IMO
we should make the interfaces safe so `Gramlib.Grammar` does provide
only one signature.