walker (Feb 08 2022 at 20:20): walker (Feb 08 2022 at 20:20):Hello everyone,
I am new to coq and I am following MIT 6.826
coq doesn't like this line:
Require Import Omega.
It says Cannot find a physical path bound to logical path Omega.
Is Omega depreciated or something ? my current coqc is 8.15.0
Olivier Laurent (Feb 08 2022 at 20:30):It has been replaced by Lia (and the omega tactic by lia).
walker (Feb 08 2022 at 20:34):well I replaced the require statement but there is some other problems that I don't fully understand:
Class EqualDec A :=
equal_dec : forall x y : A, { x = y } + { x <> y }.
(**
We define the notation [x == y] to mean our decidable equality
between [x] and [y].
*)
Notation " x == y " := (equal_dec (x :>) (y :>)) (no associativity, at level 70).
coq doesn't like the :> part on the last line I would imagine that this is part of the removed syntax in Omega ?
walker (Feb 08 2022 at 20:35):I am not even sure what to google because :> doesn't give much clues
Guillaume Melquiond (Feb 08 2022 at 20:43)::> is a very obscure feature of Coq which no one really understood what it was doing, so it got removed. It is unrelated to Omega.
walker (Feb 08 2022 at 20:53):Alright thanks, I will take this as a sign that perhaps I should install the exact coq version they used, It would be hard to learn and troubleshoot at the same time.
Paolo Giarrusso (Feb 08 2022 at 22:50):Yep, that's the correct conclusion
Michael Soegtrop (Feb 09 2022 at 08:36):@walker : if you tell me what Coq version it was, I can add it to the current Coq Platform (there was some discussion on how far back we should go).
walker (Feb 09 2022 at 08:43):8.12.0
Michael Soegtrop (Feb 09 2022 at 09:15):OK, that is already included (that is you can install this version of Coq from sources with the latest Coq Platform scripts - or you can use the published Coq Platform installers for 8.12).
walker (Feb 09 2022 at 09:29):Alright thanks, I will get it from there!
Notification Bot (Feb 09 2022 at 13:44):walker has marked this topic as resolved.
Notification Bot (Feb 09 2022 at 13:44):walker has marked this topic as unresolved.
Notification Bot (Feb 09 2022 at 13:44):walker has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC