Stream: Coq users

Topic: Building a toplevel


view this post on Zulip Chantal Keller (Apr 11 2024 at 10:08):

Hi
I try to build an OCaml toplevel which is aware of Coq using this documentation: https://coq.inria.fr/doc/V8.19.0/refman/practical-tools/utilities.html#using-coq-as-a-library
I have Coq 8.19 through opam, so I went to the directory ~/.opam/[switch name]/.opam-switch/sources/coq in order to have topbin/coqtop_bin.ml.
But I get the error: ocamlfind: Package 'coq.toplevel' not found
Thanks for your help!

view this post on Zulip Chantal Keller (Apr 20 2024 at 07:22):

No idea?

view this post on Zulip Guillaume Melquiond (Apr 21 2024 at 12:51):

I don't think there is a package named coq.toplevel. At the very best, assuming it exists, it will be named coq-core.toplevel.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:51):

Yup, seems like the documentation got outdated, should be coq-core

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:53):

@Chantal Keller what's your use case? Maybe you could save some work by re-using some of the existing toplevels like sertop or fcc

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:54):

I wrote that documentation some time ago, but it is actually a bit outdated I think (these days updating the dune file for debugging for example would work much better)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:54):

Please open a bug so we can look at the doc and fix it.

view this post on Zulip Chantal Keller (Apr 22 2024 at 16:07):

Hi
Thanks for your answers!
With coq-core, I get another error message:

Error: Could not find the .cmi file for interface topbin/coqtop_bin.mli

How can I compile it?
Should I open a bug report now or should we continue here and then I propose a patch for the documentation?
@Emilio Jesús Gallego Arias I just wanted to run a simple OCaml program without making a package and so on.

view this post on Zulip Karl Palmskog (Apr 22 2024 at 17:30):

even for a small program that uses Coq's API, the best solution is likely to make a standalone directory with a dune file that has the right (libraries ...) declaration, similar to a Coq plugin: https://github.com/coq-community/aac-tactics/blob/master/src/dune

view this post on Zulip Gaëtan Gilbert (Apr 22 2024 at 17:32):

what do you call a "toplevel" exactly?

view this post on Zulip Chantal Keller (Apr 22 2024 at 18:53):

@Gaëtan Gilbert what the documentation suggests :sweat_smile:

view this post on Zulip Chantal Keller (Apr 22 2024 at 18:54):

@Karl Palmskog If it is not possible anymore, fair enough, then it should be simply removed from the documentation

view this post on Zulip Karl Palmskog (Apr 22 2024 at 18:58):

yes, I'd say that this part of the manual is completely obsoleted by Dune. May be better to link to some example standalone tutorials for using Coq programmatically, such as https://github.com/coq-community/coq-plugin-template

view this post on Zulip Gaëtan Gilbert (Apr 22 2024 at 19:21):

the doc says

In previous versions, coqmktop was used to build custom toplevels - for example for better debugging or custom static linking. Nowadays, the preferred method is to use ocamlfind.

this doesn't define "toplevel" so I still don't know what it means

view this post on Zulip Karl Palmskog (Apr 22 2024 at 19:29):

I think there used to be all this rage about building a custom ML toplevel prompt / REPL loop (SML, OCaml), with extra features built in, like special parsing and functions. For example, the HOL4 theorem prover is basically a modified SML toplevel (has the proof and thm types loaded, etc). See also Candle, that simulates the OCaml toplevel to be like HOL Light: https://cakeml.org/candle/

view this post on Zulip Emilio Jesús Gallego Arias (Apr 26 2024 at 13:16):

Chantal Keller said:

With coq-core, I get another error message:

Error: Could not find the .cmi file for interface topbin/coqtop_bin.mli

How can I compile it?

Oh indeed, we have now a .mli file for that file too, so a manual compilation setup is:

$ make world
$ dune exec -- ocamlfind ocamlopt -thread -linkall -linkpkg -package coq-core.toplevel,coq-core.plugins.ltac -I topbin topbin/coqtop_bin.ml{i,} -o my_toplevel.native

Indeed, using dune these days is more convenient.

Should I open a bug report now or should we continue here and then I propose a patch for the documentation?
Emilio Jesús Gallego Arias I just wanted to run a simple OCaml program without making a package and so on.

I have same question that Gaëtan, what do you mean by a "simple OCaml program" ?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 26 2024 at 13:17):

A "Coq toplevel" is historicall coqtop, and variations of it, for example, linking some plugins statically

view this post on Zulip Chantal Keller (Apr 28 2024 at 06:28):

Thanks for all your answers, I have reported a bug.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2024 at 17:33):

Thanks @Chantal Keller


Last updated: Jun 13 2024 at 19:02 UTC