<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/dev/shim, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Dune: fix coqbyte shim after byterun-&gt;coqrun renaming</title>
<updated>2021-04-07T09:20:16+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2021-04-07T09:20:16+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=28599bb6760590b8040b1d09936507e4aa7dd980'/>
<id>28599bb6760590b8040b1d09936507e4aa7dd980</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[build] Split stdlib to it's own opam package.</title>
<updated>2021-03-03T15:06:14+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-06-22T15:52:18+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ab98d847d237af3cd0e46edef42218be65cfc98f'/>
<id>ab98d847d237af3cd0e46edef42218be65cfc98f</id>
<content type='text'>
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.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
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.
</pre>
</div>
</content>
</entry>
<entry>
<title>dune: Don't echo "$(pwd)" when creating the shims</title>
<updated>2020-11-30T15:40:37+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2020-11-30T15:40:37+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=81bc69df73d20c5c4d0e1ccc77255c0c6c118abc'/>
<id>81bc69df73d20c5c4d0e1ccc77255c0c6c118abc</id>
<content type='text'>
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from
different paths (typically different git worktrees).
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from
different paths (typically different git worktrees).
</pre>
</div>
</content>
</entry>
<entry>
<title>Dune: do not use with-outputs-to for shims</title>
<updated>2019-07-21T15:10:46+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2019-07-21T15:10:46+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9b929e16b1123674c737c1cef2002f5a3c3f2d39'/>
<id>9b929e16b1123674c737c1cef2002f5a3c3f2d39</id>
<content type='text'>
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] Fix shim quoting and add coqc wrapper.</title>
<updated>2019-03-28T16:18:25+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-03-28T16:18:25+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5408978c2ed5ffb4da885f742cd808bc0b518021'/>
<id>5408978c2ed5ffb4da885f742cd808bc0b518021</id>
<content type='text'>
The quoting was incorrect thus scripts didn't properly work.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
The quoting was incorrect thus scripts didn't properly work.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] Add shim for coqtop.byte</title>
<updated>2019-03-12T11:17:22+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-03-12T11:07:56+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=430851db6db8ba30280f024ccbca5f6124287ab7'/>
<id>430851db6db8ba30280f024ccbca5f6124287ab7</id>
<content type='text'>
We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.

Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.

As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.

This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.

Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.

As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.

This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] Shim for starting `coqtop/coqide` with minimal config.</title>
<updated>2019-03-03T16:21:13+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-11-21T19:16:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9870e1f8662923d0de1b9c2014d3b4f647a893da'/>
<id>9870e1f8662923d0de1b9c2014d3b4f647a893da</id>
<content type='text'>
As requested by Gaëtan Gilbert, we add shims

- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`

that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.

`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states &amp;&amp; bin/coqtop` under the old model.

This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.

In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]

We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.

The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.

This will work for `dir=stdlib/Init/` for example, or for any other
combination.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
As requested by Gaëtan Gilbert, we add shims

- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`

that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.

`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states &amp;&amp; bin/coqtop` under the old model.

This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.

In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]

We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.

The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.

This will work for `dir=stdlib/Init/` for example, or for any other
combination.
</pre>
</div>
</content>
</entry>
</feed>
