CODEWITHSUNDEEP
coq
147pm
147pm

Reputation: 2239

Coq make failing on Omega

I'm trying to follow this but the provided source files are failing make with this error

make[1]: Entering directory '/home/myhome/Dropbox/org/coq/cpdt'
COQC src/CpdtTactics.v
File "./src/CpdtTactics.v", line 10, characters 0-32:
Error: Cannot find a physical path bound to logical path Omega.

in CpdtTactics.v there is

...
Require Import Eqdep List Omega.
...

Where is this Omega? One reference mentioned it being deprecated. Another might have mentioned ZArith as a substitute. Also, just calling up InductiveTypes.v of the cpdt/src files and trying to evaluate line-by-line, I get

Error: Cannot find a physical path bound to logical path Cpdt.CpdtTactics.

I've got this in my custom-set-variables

'(coq-prog-args
   '("-emacs -R /home/myhome/Dropbox/org/coq/cpdt/src Cpdt"))

But I'm guessing this is not necessarily my mistake, rather, coq is looking for CpdtTactics.vo and it's not there because make didn't complete? (In fact, it's not there.)

I'm on coq 8.15 and am using Emacs 28.1/Proof General Version 4.5-git.

BTW, on https://x80.org/collacoq/ Require Import Omega. seems to succeed.

Upvotes: 2

Views: 461

Answers (1)

Zimm i48
Zimm i48

Reputation: 3061

The Omega module and the omega tactic have been removed in Coq version 8.14 (after being deprecated in version 8.12).

It seems that the latest CPDT tarball was not updated yet to be compatible with Coq 8.14, so this means that you should compile it with a lower version of Coq, such as version 8.13.

You can install earlier versions of Coq by relying on the Coq Platform.

If you use the Coq Platform scripts, you can rely on the latest version of the Coq Platform since it provides the option to select an earlier version of Coq. If you'd rather use the binary installers, then you can find installers for Coq 8.13 in a previous release of the Platform.

The reason why Require Import Omega works on https://x80.org/collacoq is that this website has not been kept up-to-date and is still at Coq version 8.11. If you use https://coq.vercel.app/scratchpad.html instead, you get the latest version of Coq (and thus Require Import Omega does not work).

Upvotes: 4

Related Questions