Stream: Coq users

Topic: Coq suddenly fails to build


view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:10):

I don't remember changing anything or upgrading coq, but what used to work suddenly fails with _unknown option_ errors, which seem entirely unrelated to my code.

I have a pretty basic _CoqProject file containing:

-Q . LF
Basics.v
Induction.v
Lists.v
Poly.v
Tactics.v

This is used to generate a makefile using:

coq_makefile -f _CoqProject -o Makefile

I'll then try to build using make, and get:

Unknown option -sources-of
Usage summary:

coq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]
...

I have no idea what's wrong, nor even where to begin looking. Does anybody have a hint?

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:18):

if it's any help, I'm getting the following error when trying to work with things that were already compiled:

Error: File [elided]/Tactics.vo has bad
version number 81601 (expected 81700). It is corrupted or was compiled with another
version of Coq.

So I guess there must have been some sort of automated update. I'm running Coq 8.17.1, is there an issue with the way this generates makefiles?

view this post on Zulip Rodolphe Lepigre (Sep 24 2023 at 14:25):

You probably just need to run make clean or whatever target deletes all the .vo files in the source tree. Seems like the .vo files that are present in the file system have been compiled with 8.16.1.

view this post on Zulip Rodolphe Lepigre (Sep 24 2023 at 14:26):

Also, if you're using opam, you might need to run eval $(opam env) in your shell to make sure your environment is setup correctly (for the right "switch").

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:26):

I have, but this seems unrelated. It feels like the generated Makefile is incompatible with the more recent version of coq

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:27):

the Makefile.conf file (cleanly regenerated) contains the following line:

COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))

And -sources-of is not a valid coq_makefile option

view this post on Zulip Rodolphe Lepigre (Sep 24 2023 at 14:28):

I see, then I don't know: I don't use coq_makefile much these days. Maybe someone else knows what is happening.

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:29):

I wish I wasn't using coq_makefile either, but that's the only way I could get ProofGeneral to handle Require statements...

view this post on Zulip Gaëtan Gilbert (Sep 24 2023 at 14:29):

it is valid since 8.17 https://github.com/coq/coq/pull/16308
do you have COQBIN set? It may be that which coq_makefile and $COQBIN/coq_makefile aren't the same

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:30):

I do not! What should it be set to, the path to coqc ?

view this post on Zulip Gaëtan Gilbert (Sep 24 2023 at 14:31):

leaving it unset should be fine

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:31):

it doesn't appear to be :/

view this post on Zulip Gaëtan Gilbert (Sep 24 2023 at 14:33):

what does coqc -version say?
what is COQMAKEFILE_VERSION in the generated makefile? (the main one, not the generated Makefile.conf)

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:34):

$ coqc --version
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.1

$ grep -r COQMAKEFILE_VERSION .
./Makefile:COQMAKEFILE_VERSION:=8.17.1

view this post on Zulip Gaëtan Gilbert (Sep 24 2023 at 14:36):

what does coq_makefile -sources-of say?

view this post on Zulip Karl Palmskog (Sep 24 2023 at 14:36):

it sounds like you're using a Coq Snap, and the Snap was recently updated from 8.16.1 to 8.17.1

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:37):

$ coq_makefile -sources-of
Unknown option -sources-of

view this post on Zulip Karl Palmskog (Sep 24 2023 at 14:37):

I'd recommend using a Makefile like this one, then running make clean a few times, then running make. All the .conf files need to go.

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:39):

@Karl Palmskog this is suffering from the exact same issue, since it runs coq_makefile which still appears to generate "invalid" makefiles

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:41):

now the fact that running coq_makefile -sources-of fails is maybe a hint that it's not running the right version of coq_makefile ?

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:41):

which is hard to verify since there doesn't appear to be a flag for checking coq_makefile's version...

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:42):

and yes, I absolutely am using a a Coq Snap, this one: https://snapcraft.io/install/coq-prover/ubuntu

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:47):

Well, I've temporarily worked around the issue by removing the snap and installing the standard Ubuntu package (which is still on 8.15.0)

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:48):

that's good enough for me, but I'm sure I wont' be the only one to have this issue with the snap, right?

view this post on Zulip Karl Palmskog (Sep 24 2023 at 14:50):

you can lock your coq-prover Snap to the version with Coq 8.16.1.

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 14:51):

if I find myself suffering from being on an older version I will, thanks!

view this post on Zulip Gaëtan Gilbert (Sep 24 2023 at 15:01):

Nicolas Rinaudo said:

$ coq_makefile -sources-of
Unknown option -sources-of

your coq_makefile isn't 8.17

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 15:03):

@Gaëtan Gilbert it's generated by coq_makefile though

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 15:03):

oh, sorry, misread. Yeah, that was my interpretation as well

view this post on Zulip Nicolas Rinaudo (Sep 24 2023 at 15:04):

but then again, it's the coq_makefile that was installed with the official Coq snap, and the only one available on my system, so I'd guess that there might be an issue with the snap?

view this post on Zulip Paolo Giarrusso (Sep 24 2023 at 22:10):

What does which coq_makefile output?

view this post on Zulip Paolo Giarrusso (Sep 24 2023 at 22:11):

Potentially relevant from your link:

Either log out and back in again, or restart your system, to ensure snap’s paths are updated correctly.

view this post on Zulip Paolo Giarrusso (Sep 24 2023 at 22:20):

https://github.com/coq/platform/blob/main/doc/README_Linux.md#using-non-aliased-tools-from-the-command-line might be relevant (guess not, except to test things until a new login)

view this post on Zulip Karl Palmskog (Sep 25 2023 at 06:19):

right, inconsistent coq_makefile/coqc versions can't be solved at the Coq level

view this post on Zulip Karl Palmskog (Sep 25 2023 at 06:20):

but as soon as coq_makefile/coqc are the same version, the whole build should work after cleaning out .conf and .vo files

view this post on Zulip Nicolas Rinaudo (Sep 25 2023 at 06:40):

I've removed snap, logged out and back in, installed the latest version of the snap, logged out and back in, removed every file except for *.v and _CoqProject, ran coq_makefile -f _CoqProject -o Makefile followed by make and I get the exact same error.

I've also confirmed that coq_makefile pointed to the snap-installed one, as did coq.

view this post on Zulip Nicolas Rinaudo (Sep 25 2023 at 06:41):

as I said, getting rid of the snap and using the standard Ubuntu package, stuck on 8.15.0, works for me. But the symptoms make me suspect that the problem is not with my setup, but the snap itself

view this post on Zulip Karl Palmskog (Sep 25 2023 at 06:49):

you can try manually adding this at the top of your PATH: /snap/coq-prover/current/coq-platform/bin

For example:

export PATH=/snap/coq-prover/current/coq-platform/bin:$PATH

Then which coq_makefile and which coqc should give the expected ones

view this post on Zulip Karl Palmskog (Sep 25 2023 at 06:50):

@Michael Soegtrop I can see that the 2023.03 Snap provides an executable coq-prover.coq-makefile in the path (note the dash), this may be related to troubles above

view this post on Zulip Huỳnh Trần Khanh (Sep 25 2023 at 09:18):

Nicolas Rinaudo said:

as I said, getting rid of the snap and using the standard Ubuntu package, stuck on 8.15.0, works for me. But the symptoms make me suspect that the problem is not with my setup, but the snap itself

Correct. I had the exact same problem a few days ago. This is not an isolated incident.

view this post on Zulip Paolo Giarrusso (Sep 25 2023 at 10:51):

cc @Michael Soegtrop

view this post on Zulip Karl Palmskog (Sep 25 2023 at 11:43):

@Michael Soegtrop I reproduced the Snap problem locally with 8.17. The only plausible explanation I can think of is that coq_makefile in the 8.17 channel (2023.03/stable) is actually from 8.16 (where the -sources-of option doesn't exist), the packaging of the Snap uses the wrong one.

@Nicolas Rinaudo this is how you can lock your Snap to 8.16 that works until the 8.17 Snap is fixed:

sudo snap refresh coq-prover --channel=2022.09/stable

view this post on Zulip Nicolas Rinaudo (Sep 25 2023 at 11:45):

Thanks @Karl Palmskog ! I'm actually fine staying on 8.15.0 for the moment - kind of been burned by spending an afternoon fixing this rather than learning Coq as I'd hoped, so while it's working, I ain't touching it :)

view this post on Zulip Karl Palmskog (Sep 25 2023 at 11:46):

fine by me, but I at least validated the locking with --channel=2022.09/stable works locally.

view this post on Zulip Michael Soegtrop (Sep 25 2023 at 16:21):

I currently don't have access to a Linux machine. I can look into it tomorrow evening.
@Karl Palmskog : the snap is built in a clean VM - if there is some mix of Coq versions going on, the only plausible explanation is that something is going wrong with opam. I can't exclude that I messed up with the opam patches in the Coq Platform repo. Would you mind taking a look?

view this post on Zulip Karl Palmskog (Sep 25 2023 at 16:48):

it seems unlikely that opam could have caused mixing of coqc from 8.17.1 with coq_makefile from 8.16.1 (those executable are both part of the coq-core package). It may be something with the Snap production process

view this post on Zulip Michael Soegtrop (Sep 25 2023 at 17:03):

As I said, the snap is built in a clean VM - it is not possible that there are left overs from the previous build.

view this post on Zulip Michael Soegtrop (Sep 25 2023 at 17:04):

But I will find out when I am back home and have access to my Linux machine,

view this post on Zulip Karl Palmskog (Sep 25 2023 at 18:25):

when I do this, all the coq_makefile troubles with Snap disappear:

export PATH=/snap/coq-prover/current/coq-platform/bin/:$PATH

Then, I'm consistently using 8.17.1 stuff.

However, the current Snap includes a bunch of 8.16 binaries here: /snap/coq-prover/31/coq-platform/bin/ (current is a symlink to 32, where 8.17 things live). What I think is happening is that coq_makefile in /snap/bin actually invokes /snap/coq-prover/31/coq-platform/bin/coq_makefile instead of /snap/coq-prover/32/coq-platform/bin/coq_makefile.

view this post on Zulip Karl Palmskog (Sep 25 2023 at 18:28):

I have no idea how the Snap indirection works for things in /snap/bin, e.g., /snap/bin/coq_makefile -> coq-prover.coq-makefile and /snap/bin/coq-prover.coq-makefile -> /usr/bin/snap (symlinking), so I don't know where it's determined what coq-prover.coq-makefile actually maps to when given as argument to /usr/bin/snap.

But when using directly the binaries in /snap/coq-prover/current/, there is no indirection, and then it works.

view this post on Zulip Karl Palmskog (Sep 25 2023 at 18:31):

@Enrico Tassi do you know where the mapping between what is in /snap/bin and what is in /snap/<package>/<version>/bin is defined?

view this post on Zulip Enrico Tassi (Sep 25 2023 at 19:54):

Stuff like coq-prover.coqide is defined in the snapcraft.yaml file (https://github.com/coq/platform/blob/9efe1bfc3653875e57a4ab553b915548cf6b9d69/linux/snap/snapcraft.yaml.in#L57), while short names (aliases) are global to the snap store, see the comment in the same file

view this post on Zulip Karl Palmskog (Sep 25 2023 at 19:58):

then it could be that the Snap store causes the problem with misdirected coq_makefile alias, I can't really tell

view this post on Zulip Karl Palmskog (Sep 25 2023 at 20:25):

everything boils down to:

$ /snap/bin/coq_makefile -sources-of
Unknown option -sources-of

$ /snap/coq-prover/current/coq-platform/bin/coq_makefile -sources-of

$ /snap/coq-prover/32/coq-platform/bin/coq_makefile -sources-of

$ /snap/coq-prover/31/coq-platform/bin/coq_makefile -sources-of
Unknown option -sources-of

$ /snap/bin/coq-prover.coq-makefile -sources-of
Unknown option -sources-of

view this post on Zulip Gaëtan Gilbert (Sep 25 2023 at 20:46):

realpath /snap/bin/coq_makefile?

view this post on Zulip Karl Palmskog (Sep 25 2023 at 21:07):

as per above,

$ realpath /snap/bin/coq_makefile
/usr/bin/snap

So it goes into the snap indirection machinery.

view this post on Zulip Gaëtan Gilbert (Sep 25 2023 at 21:09):

oh snap

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 04:24):

The way this discussion went down the wrong path is impressive. (But I admit the evidence is quite misleading.) The situation is much simpler than that. There is no confusion on the snap side, it is the correct coq_makefile that is being run. The issue is that -sources-of needs to be the very first argument of coq_makefile to be recognized (don't ask why). But when run from the snap, it becomes the second argument, because the first argument is COQBIN=..., thus everything breaks.

view this post on Zulip Enrico Tassi (Sep 26 2023 at 08:25):

I'll open an issue on the platform

view this post on Zulip Enrico Tassi (Sep 26 2023 at 08:27):

https://github.com/coq/platform/issues/366
Thanks for debugging

view this post on Zulip Théo Zimmermann (Sep 26 2023 at 08:29):

IMO this would also deserve a fix to coq_makefile, to make it more robust.

view this post on Zulip Karl Palmskog (Sep 26 2023 at 08:29):

can't the COQBIN = ... just be moved to before the coq_makefile call?

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 08:30):

I don't think coq_makefile reads the actual environment to know how to fill the Makefile; it just reads the command line.

view this post on Zulip Enrico Tassi (Sep 26 2023 at 08:32):

The quick fix is to move COQBIN= after the other arguments, it can be done in the snap wrapper I think.
Fixing coq_makefile is also an option, but requires more time to get in the snap.

view this post on Zulip Enrico Tassi (Sep 26 2023 at 08:34):

https://github.com/coq/platform/pull/367

view this post on Zulip Michael Soegtrop (Sep 26 2023 at 10:35):

@Karl Palmskog

However, the current Snap includes a bunch of 8.16 binaries here: /snap/coq-prover/31/coq-platform/bin/ (current is a symlink to 32, where 8.17 things live).

The things in folder 31 and 32 are different snaps. Whenever you install a new version of the Coq Platform snap, this number is incremented. A certain number of previous variants is kept. The number is not a snap version - it depends on your local install history. That is, if you install Coq Platform for the first time, this number is one.

So it is natural that different folders contain different coq versions. If you have the impression that things get mixed up, you should check your PATH.

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 11:28):

Michael Soegtrop said:

The number is not a snap version - it depends on your local install history. That is, if you install Coq Platform for the first time, this number is one.

No, this is really a snap version. For example, I have never installed coq-prover on this computer, yet I get the same revision numbers as Karl:

$ snap info coq-prover
name:      coq-prover
...
channels:
  latest/stable:     2023-03-0 2023-09-18 (32) 811MB -
  ...
  2022.09/stable:    2022-09-1 2023-01-16 (31) 791MB -
  ...

Notice the (31) and (32).

view this post on Zulip Enrico Tassi (Sep 26 2023 at 12:22):

I believe each upload to the store gets a new number, so last release was upload number 32.
A package installed by hand gets something like x1.

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 07:43):

Now that the problem is understood and a fix is proposed, would it be difficult to re-upload a Snap quickly? Who is able to do it besides @Michael Soegtrop in case he doesn't have time for this? @Enrico Tassi? @Romain Tetley? This seems like a quite urgent matter that the default install of Coq in Snap ships a broken coq_makefile.

view this post on Zulip Michael Soegtrop (Sep 28 2023 at 07:44):

@Guillaume Melquiond : Interesting. Possibly things are different if one installs a lot of locally build snaps, as I do. For me the numbers are not the same as for you and Karl.

view this post on Zulip Michael Soegtrop (Sep 28 2023 at 07:45):

@Théo Zimmermann : I will rebuild the snap and upload a fix today.

view this post on Zulip Michael Soegtrop (Sep 28 2023 at 12:38):

I uploaded the new version as latest/candidate and 2023.03/candidate. @Nicolas Rinaudo : can you please test this?

view this post on Zulip Karl Palmskog (Sep 28 2023 at 12:39):

for reference:

sudo snap refresh coq-prover --channel=2023.03/candidate

view this post on Zulip Michael Soegtrop (Sep 28 2023 at 12:47):

@Guillaume Melquiond : you are right. For me the folders are all named x<number> (with a literal x in front) and these start with 1 and increase on each install, but this x<number> notation is only used for local builds. The folders named just <number> are from installs from the official snap store and here indeed the number is the upload index to snap.

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 12:38):

@Nicolas Rinaudo : did you already have a chance to test the updated snap?

view this post on Zulip Nicolas Rinaudo (Sep 29 2023 at 12:58):

I just did, and am facing exactly the same problem I'm afraid

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:07):

How can I reproduce it? A simple coq_makefile based make with 2 dependent .v files would suffice?

view this post on Zulip Nicolas Rinaudo (Sep 29 2023 at 13:09):

Yes. Here's my _CoqProject, to show you that there's nothing special going on:

-Q . LF
Basics.v
Induction.v
Lists.v
Poly.v
Tactics.v

I'll then run:

coq_makefile -f _CoqProject -o Makefile
make

And this fails immediately.

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:12):

OK, I will try this. Currently I don't have platform level tests for coq makefile (usually such things are found at coq-core CI).

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:13):

I guess I need to add a coq_makefile test to the smoke test kit.

view this post on Zulip Nicolas Rinaudo (Sep 29 2023 at 13:13):

I'm sorry, as a complete Coq beginner, I have very little to contribute here other than checking weither things work for me

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:14):

That's perfectly fine. I see it as my job to deliver a platform which works well under almost all circumstances.

view this post on Zulip Nicolas Rinaudo (Sep 29 2023 at 13:19):

Thankless job. So let me thank you, I know how tough it can be.

view this post on Zulip Karl Palmskog (Sep 29 2023 at 13:27):

@Michael Soegtrop I've tested locally that 2023.03/candidate indeed solves the coq_makefile issue

view this post on Zulip Nicolas Rinaudo (Sep 29 2023 at 13:31):

Apologies. I was the problem - should have read this more carefully, I didn't follow the right steps for upgrading. Now that I have, it's working.

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:31):

@Nicolas Rinaudo : since it works for Karl: are you sure you installed the update and possibly set your PATH to use this new installation?

How are you using the snap? I guess you added /snap/coq-prover/current/coq-platform/bin/ to your PATH, since you are not using the alias names under /snap/bin (which would e.g. be coq-prover.coq-makefile instead of coq-makefile. If so, please be sure to use /current/ in your path and not /32/ or /33/.

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:32):

Overlapping posts. So all is well then (except that since this change the Snap CI fails consistently with disk full - sigh).

view this post on Zulip Karl Palmskog (Sep 29 2023 at 13:34):

I even did some back-and-forth switching now between 2023.03/candidate and 2023.03/stable, behaves as expected on a coq_makefile-based project

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 13:45):

@Karl Palmskog : thanks. So I guess the conclusion is that I promote candidate to stable in 2023.03 and latest?

view this post on Zulip Karl Palmskog (Sep 29 2023 at 13:46):

right, in my view you should promote 2023.03/candidate to 2023.03/stable as soon as possible.

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 14:06):

I promoted candidate to stable, created a new tag 2023.03.1 and updated the notes in the release (stating that only snap was affected, so I kept the 2023.03.0 installers for Windows and macOS).

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 14:08):

@Karl Palmskog : do you think it is problematic to have a release 2023.03.0 on macOS and Windows and 2023.03.1 on snap? This might lead to some minor confusion but then running the whole process for no changes at all seems to be too much effort for the little gain of consistent release numbers.

view this post on Zulip Karl Palmskog (Sep 29 2023 at 14:11):

can't you just put copies of the 2023.03.0 installers for macOS and Windows in the 2023.03.1 release also?

view this post on Zulip Karl Palmskog (Sep 29 2023 at 14:11):

I don't know what is best to do, I personally only use Snap or install scripts

view this post on Zulip Michael Soegtrop (Sep 29 2023 at 15:39):

@Karl Palmskog : I didn't really do a 2023.03.1 release - I called the existing one 2023.03.0/.1.

view this post on Zulip Théo Zimmermann (Sep 29 2023 at 15:43):

@Michael Soegtrop I think what you did is fine in this case.


Last updated: Jun 23 2024 at 05:02 UTC