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.
can you show what your dune
file looks like?
$ 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)
If I didn't use the noinit flag I would probably not even need to point to the numeral_notation plugin.
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))
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
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
Ah, I just noticed that there is no dune file in 8.11
in the plugins folder
right, so you may want to try compiling v8.12
or master
with dune and see if it works
I switched to 8.12 and ocamlfind still can't find it
but did you compile Coq with dune? That doesn't happen with opam packages and so on.
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
I compiled it with opam
And it turns out that numeral_notation
is missing from there.
So it's not surprising that you see this error.
If you build Coq from sources using Dune like Karl suggests, the generated META file will probably be correct.
But it seems to me that] this is also a bug of the current META file (worth reporting).
Ah excellent. Is there a way to get opam to do that for me?
Probably yes.
I'm not an opam expert though.
you could try pinning the coq.opam
file in a checked out Coq clone: opam pin add coq -k path .
Alright, thanks for the help! I'll let you know if I succeed. In the meantime I will submit an issue
Here is the issue:
https://github.com/coq/coq/issues/12789
Hmm I am having trouble building coq with dune. I'm just supposed to run dune build
in the coq clone right?
I uninstalled coq from my opam switch to do this
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
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
.
Ah I misunderstood. So opam will use dune for me
yes, if you look at coq.opam
contents for the clone, you see it uses dune
Success!
$ ocamlfind query -i-format coq.plugins.numeral_notation
-I /home/ali/.opam/coq-8.11.2/lib/coq/plugins/numeral_notation
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
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.
$ opam install coqide-server
[ERROR] No package named coqide-server found.
$ opam pin add coqide-server.8.11.2 -k path .
Package coqide-server does not exist, create as a NEW package? [Y/n] n
I have coqide-server.opam though...
@Ali Caglayan versions like 8.11.2 don't work for local packages in cloned Coq repos
Does it work on 8.12?
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 .
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
Its prompting me to create as a new package
yes, that's normal.
Hmm this doesn't seem right:
The following dependencies couldn't be met:
- coqide-server → coq < 8.3
no matching version
you have to install coqide-server
first, and it should have version dev
when doing opam list
.
Thats the message I get when trying to install coqide-server
$ 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
And opam install coqide-server.dev
doesn't seem to work.
[ERROR] Package coqide-server has no version dev.
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
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
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.
OK, thanks for your help. I will try this in 8.12 then
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
hmm, isn't it an open secret that CoqIDE works fine with other versions of Coq than the one it's tied to?
so you could use a CoqIDE from another opam switch to work with the custom Coq executable in your current switch
How do you do that?
you have to manually find/run the coqide
executable in $HOME/.opam/other-switch/path/to/coqide
Oh, I see
I tried coqide 8.12 but I get a bad magic number error
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.
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
.
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
You mean there was no new release? Because the master
branch should be compatible with Coq 8.12.
And you can probably install it from the coq-extra-dev
repository.
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.
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
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
Nice, I've managed to get the HoTT library to work without the stdlib and with dune :-)
Last updated: Oct 13 2024 at 01:02 UTC