Stream: Coq devs & plugin devs

Topic: ocamlfind numeral_notation


view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:46):

Hi, I've been trying to list the numeral_notation plugin as a dune dependency in my project. Dune tells me this:

File "theories/dune", line 8, characters 4-32:
8 |     coq.plugins.numeral_notation
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.numeral_notation" not found.
Hint: try: dune external-lib-deps --missing @@default

But I think the problem is with ocamlfind since the following doesn't work:

$ ocamlfind query -i-format coq.plugins.numeral_notation
ocamlfind: Package `coq.plugins.numeral_notation' not found

But ocamlfind can find other plugins like ltac and ssreflect:

$ ocamlfind query -i-format coq.plugins.ltac
-I /home/ali/.opam/coq-8.11.2/lib/coq/plugins/ltac
$ ocamlfind query -i-format coq.plugins.ssreflect
-I /home/ali/.opam/coq-8.11.2/lib/coq/plugins/ssr

Am I using the right name for the numeral_notation plugin? Can anybody else confirm that ocamlfind can find it? I've only seen the plugin being mentioned in the coq stdlib dune file.

view this post on Zulip Karl Palmskog (Aug 03 2020 at 12:50):

can you show what your dune file looks like?

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:51):

$ cat theories/dune
(coq.theory
  (name HoTT)
  (package hott)
  (synopsis "The HoTT library.")
  (libraries
    coq.plugins.ltac
    coq.plugins.extraction
    coq.plugins.numeral_notation
    coq.plugins.string_notation
;    coq.plugins.int63_syntax
;    coq.plugins.r_syntax
;    coq.plugins.float_syntax

    )
  (flags -noinit -indices-matter))

(include_subdirs qualified)

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:53):

If I didn't use the noinit flag I would probably not even need to point to the numeral_notation plugin.

view this post on Zulip Karl Palmskog (Aug 03 2020 at 12:54):

hmm, it looks indeed like you're using the right public name:

(library
 (name numeral_notation_plugin)
 (public_name coq.plugins.numeral_notation)
 (synopsis "Coq numeral notation plugin")
 (modules g_numeral numeral)
 (libraries coq.vernac))

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:55):

These don't seem to work:

$ ocamlfind query -i-format coq.plugins.syntax
ocamlfind: Package `coq.plugins.syntax' not found
$ ocamlfind query -i-format coq.plugins.syntax.numeral_notation
ocamlfind: Package `coq.plugins.syntax.numeral_notation' not found

In the dune file in coq/theories on master you can see numeral_notation is included the way I wrote it: https://github.com/coq/coq/blob/master/theories/dune

view this post on Zulip Karl Palmskog (Aug 03 2020 at 12:57):

this might be a question @Emilio Jesús Gallego Arias is most suited to answer definitively, but it might be the case that coq.plugins.numeral_notation is only exposed when Coq itself is compiled with dune

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:58):

Ah, I just noticed that there is no dune file in 8.11

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:58):

in the plugins folder

view this post on Zulip Karl Palmskog (Aug 03 2020 at 12:58):

right, so you may want to try compiling v8.12 or master with dune and see if it works

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:58):

I switched to 8.12 and ocamlfind still can't find it

view this post on Zulip Karl Palmskog (Aug 03 2020 at 12:59):

but did you compile Coq with dune? That doesn't happen with opam packages and so on.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 12:59):

The default installation doesn't use Dune, in 8.11 nor in 8.12, so the source of truth is this META file instead: https://github.com/coq/coq/blob/master/META.coq.in

view this post on Zulip Ali Caglayan (Aug 03 2020 at 12:59):

I compiled it with opam

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 12:59):

And it turns out that numeral_notation is missing from there.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 12:59):

So it's not surprising that you see this error.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 12:59):

If you build Coq from sources using Dune like Karl suggests, the generated META file will probably be correct.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 13:00):

But it seems to me that] this is also a bug of the current META file (worth reporting).

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:00):

Ah excellent. Is there a way to get opam to do that for me?

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 13:00):

Probably yes.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 13:00):

I'm not an opam expert though.

view this post on Zulip Karl Palmskog (Aug 03 2020 at 13:01):

you could try pinning the coq.opam file in a checked out Coq clone: opam pin add coq -k path .

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:02):

Alright, thanks for the help! I'll let you know if I succeed. In the meantime I will submit an issue

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:04):

Here is the issue:
https://github.com/coq/coq/issues/12789

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:22):

Hmm I am having trouble building coq with dune. I'm just supposed to run dune build in the coq clone right?

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:23):

I uninstalled coq from my opam switch to do this

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:23):

But I am getting these errors:

File "doc/plugin_tutorial/tuto0/src/dune", line 4, characters 12-28:
4 |  (libraries coq.plugins.ltac))
                ^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ltac" not found.
Hint: try: dune external-lib-deps --missing @@default
File "doc/plugin_tutorial/tuto1/src/dune", line 4, characters 12-28:
4 |  (libraries coq.plugins.ltac))
                ^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ltac" not found.
Hint: try: dune external-lib-deps --missing @@default
File "doc/plugin_tutorial/tuto2/src/dune", line 4, characters 12-28:
4 |  (libraries coq.plugins.ltac))
                ^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ltac" not found.
Hint: try: dune external-lib-deps --missing @@default
File "doc/plugin_tutorial/tuto3/src/dune", line 5, characters 12-28:
5 |  (libraries coq.plugins.ltac))
                ^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ltac" not found.
Hint: try: dune external-lib-deps --missing @@default

I am on 8.11

view this post on Zulip Karl Palmskog (Aug 03 2020 at 13:24):

I highly recommend not running dune build, but using the opam command above, which will use the coq.opam file which sends the right options to dune.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:24):

Ah I misunderstood. So opam will use dune for me

view this post on Zulip Karl Palmskog (Aug 03 2020 at 13:25):

yes, if you look at coq.opam contents for the clone, you see it uses dune

view this post on Zulip Ali Caglayan (Aug 03 2020 at 13:39):

Success!

$ ocamlfind query -i-format coq.plugins.numeral_notation
-I /home/ali/.opam/coq-8.11.2/lib/coq/plugins/numeral_notation

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:06):

I'm having trouble building coqide. I tried:

$ opam pin add coqide.8.11.2 -k path .

But opam is telling me this:

[NOTE] Package coqide is already pinned to file:///home/ali/repos/coq-8.11.2
       (version 8.11.2).
[coqide.8.11.2] no changes from file:///home/ali/repos/coq-8.11.2
coqide is now pinned to file:///home/ali/repos/coq-8.11.2 (version 8.11.2)

The following dependencies couldn't be met:
  - coqide → coqide-server
      unknown package

[NOTE] Pinning command successful, but your installed packages may be out of
       sync.

I'm really confused why it can't find coqide-server

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 14:17):

I think opam is stupid and tries to match what it finds in the git repository with what it knows from its own opam repository. Try installing the coqide-server package first.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:18):

$ opam install coqide-server
[ERROR] No package named coqide-server found.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:18):

$ opam pin add coqide-server.8.11.2 -k path .
Package coqide-server does not exist, create as a NEW package? [Y/n] n

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:19):

I have coqide-server.opam though...

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:26):

@Ali Caglayan versions like 8.11.2 don't work for local packages in cloned Coq repos

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:27):

Does it work on 8.12?

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:27):

you might have to do something like the following in the cloned repo:

opam pin add coqide-server -k path .
opam pin add coqide -k path .

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:28):

it will only work with the version of Coq you have cloned, I don't remember if v8.11 even has these *.opam files with dune

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:28):

Its prompting me to create as a new package

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:29):

yes, that's normal.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:30):

Hmm this doesn't seem right:

The following dependencies couldn't be met:
  - coqide-server → coq < 8.3
      no matching version

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:33):

you have to install coqide-server first, and it should have version dev when doing opam list.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:34):

Thats the message I get when trying to install coqide-server

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:35):

$ opam install coqide-server

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coqide-server.~dev] no changes from file:///home/ali/repos/coq-8.11.2

The following dependencies couldn't be met:
  - coqide-server → coq < 8.3
      no matching version

No solution found, exiting

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:35):

And opam install coqide-server.dev doesn't seem to work.

[ERROR] Package coqide-server has no version dev.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:37):

Here is my opam list if that is helpful:

# Packages matching: installed
# Name                 # Installed # Synopsis
base-bigarray          base
base-threads           base
base-unix              base
cairo2                 0.6.1       Binding to Cairo, a 2D Vector Graphics Librar
conf-cairo             1           Virtual package relying on a Cairo system ins
conf-findutils         1           Virtual package relying on findutils
conf-gnome-icon-theme3 0           Virtual package relying on gnome-icon-theme
conf-gtk3              18          Virtual package relying on GTK+ 3
conf-gtksourceview3    0+1         Virtual package relying on a GtkSourceView-3
conf-m4                1           Virtual package relying on m4
conf-pkg-config        1.2         Virtual package relying on pkg-config install
coq                    8.11.2      pinned to version 8.11.2 at file:///home/ali/
dune                   2.6.2       Fast, portable, and opinionated build system
dune-configurator      2.6.2       Helper library for gathering system configura
dune-private-libs      2.6.2       Private libraries of Dune
lablgtk3               3.1.1       OCaml interface to GTK+3
lablgtk3-sourceview3   3.1.1       OCaml interface to GTK+ gtksourceview library
num                    1.3         The legacy Num library for arbitrary-precisio
ocaml                  4.10.0      The OCaml compiler (virtual package)
ocaml-base-compiler    4.10.0      Official release 4.10.0
ocaml-config           1           OCaml Switch Configuration
ocamlfind              1.8.1       A library manager for OCaml
ocamlgraph             1.8.8       A generic graph library for OCaml

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:37):

if these are packages for the v8.11 branch, they might not work, I would try installing coq.opam, coqide-server.opam and coqide.opam from scratch on v8.12 or master

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:38):

basically, you can't have Coq pinned as some version other than dev, and by default the coq.opam package definition will give you the dev version. If opam list shows some other version of Coq when pinned, it won't work to install that version of CoqIDE.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:40):

OK, thanks for your help. I will try this in 8.12 then

view this post on Zulip Ali Caglayan (Aug 03 2020 at 14:41):

I was hoping to avoid having to go to 8.12 with the HoTT library since it hasn't been updated yet, but I guess now I will have to wait

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:46):

hmm, isn't it an open secret that CoqIDE works fine with other versions of Coq than the one it's tied to?

view this post on Zulip Karl Palmskog (Aug 03 2020 at 14:47):

so you could use a CoqIDE from another opam switch to work with the custom Coq executable in your current switch

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:01):

How do you do that?

view this post on Zulip Karl Palmskog (Aug 03 2020 at 15:03):

you have to manually find/run the coqide executable in $HOME/.opam/other-switch/path/to/coqide

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:03):

Oh, I see

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:09):

I tried coqide 8.12 but I get a bad magic number error

view this post on Zulip Karl Palmskog (Aug 03 2020 at 15:11):

sigh, so they lock it I guess. I can confirm that ProofGeneral works across many versions of Coq simultaneously, and should be the same for VsCoq.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 15:12):

CoqIDE should work across multiple versions (even if it's not supported in theory). A bad magic number seems more like your other CoqIDE is using your other coqidetop instead of the one you currently have in PATH.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 15:13):

But I'm surprised by this:

I was hoping to avoid having to go to 8.12 with the HoTT library since it hasn't been updated yet, but I guess now I will have to wait

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 15:13):

You mean there was no new release? Because the master branch should be compatible with Coq 8.12.

view this post on Zulip Théo Zimmermann (Aug 03 2020 at 15:14):

And you can probably install it from the coq-extra-dev repository.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:23):

I am currently waiting for the 8.12 release of the HoTT library to be merged (I've created a PR). The main issue was that coq-dpdgraph didn't work with 8.12. I've since sent a patch their way however.

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:29):

coqide wasn't super important for what I wanted to do anyway, I was trying to see how it would interact with dune. Once I had done a dune build I was interested in seeing how opening files in the _build folder with coqide would work

view this post on Zulip Ali Caglayan (Aug 03 2020 at 15:35):

I'm trying the local clone idea again for 8.12 to get dune to find numeral_notation. However this time I should be able to install coqide

view this post on Zulip Ali Caglayan (Aug 03 2020 at 16:49):

Nice, I've managed to get the HoTT library to work without the stdlib and with dune :-)


Last updated: Oct 21 2021 at 21:03 UTC