Stream: Coq users

Topic: ✔ Troubleshooting missing Omega


view this post on Zulip 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

view this post on Zulip Olivier Laurent (Feb 08 2022 at 20:30):

It has been replaced by Lia (and the omega tactic by lia).

view this post on Zulip 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 ?

view this post on Zulip walker (Feb 08 2022 at 20:35):

I am not even sure what to google because :> doesn't give much clues

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 22:50):

Yep, that's the correct conclusion

view this post on Zulip 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).

view this post on Zulip walker (Feb 09 2022 at 08:43):

8.12.0

view this post on Zulip 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).

view this post on Zulip walker (Feb 09 2022 at 09:29):

Alright thanks, I will get it from there!

view this post on Zulip Notification Bot (Feb 09 2022 at 13:44):

walker has marked this topic as resolved.

view this post on Zulip Notification Bot (Feb 09 2022 at 13:44):

walker has marked this topic as unresolved.

view this post on Zulip Notification Bot (Feb 09 2022 at 13:44):

walker has marked this topic as resolved.


Last updated: Feb 09 2023 at 00:03 UTC