Stream: math-comp users

Topic: ✔ From mathcomp Require Import all -- not working?


view this post on Zulip Julien Puydt (Feb 17 2022 at 15:37):

I can "From mathcomp Require Import all_algebra all_character all_field all_fingroup all_solvable all_ssreflect"... and they get found in /usr/lib/ocaml/coq/user-contrib/mathcomp/whatever/all_whatever.*, so things look bright.

But I can't "From mathcomp Require Import all" ... even though there are /usr/lib/ocaml/coq/user-contrib/mathcomp/all/all.* files. Is it a problem with the packaging of mathcomp in Debian or do I miss something obvious?

view this post on Zulip Enrico Tassi (Feb 17 2022 at 15:53):

Do we compile all.vo?

view this post on Zulip Cyril Cohen (Feb 17 2022 at 15:56):

Probably not, I think I hacked it in for nix, but forgot to make it available globally. And I guess it should be all_all, shouldn't it?

view this post on Zulip Enrico Tassi (Feb 17 2022 at 16:10):

all_mathcomp maybe?

view this post on Zulip Julien Puydt (Feb 17 2022 at 17:10):

Well:

jpuydt@phaeris:/usr/lib/ocaml/coq/user-contrib/mathcomp$ ls all/
all.glob  all.v  all.vo

so yes, all.vo is compiled. As I said, I don't know why it doesn't work, since it looks pretty much like all the other things I "From mathcomp Require Import"...

view this post on Zulip Julien Puydt (Feb 18 2022 at 12:23):

Fun fact: if I put "From mathcomp Require Import all." in a test.v file then call coqc on it by hand, I get a handful of warnings, but no error...

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 12:37):

can you compare the working and failing situations (coq version, settings, invocation... you know the drill)

view this post on Zulip Enrico Tassi (Feb 18 2022 at 13:05):

Are you saying it works in coqc but not in coqide?

view this post on Zulip Enrico Tassi (Feb 18 2022 at 13:06):

(in any case, nobody wants to load all, so I don't think this is a blocker... but I'm really interested in understanding why it does not work)

view this post on Zulip Julien Puydt (Feb 18 2022 at 17:55):

Well, the coq version is 8.15.0 ; I don't think I did anything to the settings... the invocation was just "coqc test.v" where test.v is the one-liner.

Why wouldn't anyone load all? Since this exists, I wanted to try it...

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 18:01):

@Julien Puydt you said

But I can't "From mathcomp Require Import all"

but to investigate we'll need a more proper bug report, including actual errors, paths of the binaries used in both cases, etc. I can elaborate more if needed.
If the issue isn't "two Coq binaries", it's going to be fun.

view this post on Zulip Enrico Tassi (Feb 18 2022 at 18:02):

Yes, in this thread you seem to both say that From mathcomp Require Import all. works and does not work. So I'm lost. What did you change?

view this post on Zulip Enrico Tassi (Feb 18 2022 at 18:03):

I thought one was with CoqIDE and the other with coqc, but it seems It was not the case.

view this post on Zulip Julien Puydt (Feb 18 2022 at 21:09):

In coqide, the line From mathcomp Require Import all gets an error Cannot find a physical path bound to logical path all with prefix mathcomp., while the same line in a file given to coqc gives warnings but no error.

view this post on Zulip Julien Puydt (Feb 18 2022 at 21:10):

Both coqc and coqide are run from /usr/bin, as I'm using the Debian packages

view this post on Zulip Julien Puydt (Feb 18 2022 at 21:13):

I just tried to coqidetop.opt -l test.v and I get the same warnings, and then Fatal error: ideslave communication channels not set. -- but as far as I know that's the expected error when running coqidetop from the commandline

view this post on Zulip Julien Puydt (Feb 18 2022 at 21:14):

Wait, I just restarted coqide, and the problem is gone... I have the same warnings I had with coqc.

view this post on Zulip Julien Puydt (Feb 18 2022 at 21:16):

Now I'm left wondering what could have caused the error... I didn't update the packages since long :-/

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:31):

any chance you started coqide before installing mathcomp? that could do it.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:31):

the more precise question is when you started the underlying coqidetop, but that’s less visible.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:33):

at the very least that’s often my experience with using coqidetop from VSCoq — I haven’t fully minimized it, but it feels like at least if Require fails, adding the missing .vo is not enough, I need to restart the Coq process.

view this post on Zulip Enrico Tassi (Feb 18 2022 at 22:43):

Yup, coq reads the file system once and caches it

view this post on Zulip Notification Bot (Feb 19 2022 at 09:24):

Julien Puydt has marked this topic as resolved.


Last updated: Mar 28 2024 at 15:01 UTC