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?
Do we compile all.vo?
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?
all_mathcomp maybe?
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"...
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...
can you compare the working and failing situations (coq version, settings, invocation... you know the drill)
Are you saying it works in coqc
but not in coqide
?
(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)
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...
@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.
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?
I thought one was with CoqIDE and the other with coqc, but it seems It was not the case.
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.
Both coqc and coqide are run from /usr/bin, as I'm using the Debian packages
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
Wait, I just restarted coqide, and the problem is gone... I have the same warnings I had with coqc.
Now I'm left wondering what could have caused the error... I didn't update the packages since long :-/
any chance you started coqide before installing mathcomp
? that could do it.
the more precise question is when you started the underlying coqidetop, but that’s less visible.
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.
Yup, coq reads the file system once and caches it
Julien Puydt has marked this topic as resolved.
Last updated: Mar 28 2024 at 15:01 UTC