Stream: Hydras & Co. universe

Topic: ✔ How to install (?) Goedel on windows


view this post on Zulip Lessness (Oct 03 2022 at 15:31):

I cloned the repository and want to edit/run/check/etc some files in CoqIde, but I get stuck, for example, at From hydras.Ackermann Require Import extEqualNat..

What's the best way to fix this problem? To build/install all necessary stuff?
Thanks in advance.

view this post on Zulip Pierre Castéran (Oct 03 2022 at 15:36):

Did you install hydra-battles before?

view this post on Zulip Théo Zimmermann (Oct 03 2022 at 15:37):

How have you installed Coq? Binary installer? The Coq Platform provides scripts to get a working opam environment. From then, you could install hydra-battles as suggested by Pierre.

view this post on Zulip Lessness (Oct 03 2022 at 15:40):

Pierre Castéran said:

Did you install hydra-battles before?

Uff, no. :sweat_smile: Will try to do it now.

view this post on Zulip Lessness (Oct 03 2022 at 16:09):

Okay, I installed latest Coq Platform... Can't find opam on my computer (neither using cmd nor cygwin). Have I done smth wrong?

view this post on Zulip Karl Palmskog (Oct 03 2022 at 16:10):

unfortunately, the Coq Platform currently uses a CoqPrime release incompatible with Goedel. At least Hydra Battles should build out of the box

view this post on Zulip Théo Zimmermann (Oct 03 2022 at 16:27):

Lessness said:

Okay, I installed latest Coq Platform... Can't find opam on my computer (neither using cmd nor cygwin). Have I done smth wrong?

With the Platform scripts, right? I think opam is supposed to be available through cygwin.

view this post on Zulip Karl Palmskog (Oct 03 2022 at 16:28):

(Platform installers for sure don't come with opam)

view this post on Zulip Lessness (Oct 03 2022 at 16:35):

<< The Coq platform is the recommended way to install Coq for both beginners and experts. Beginners are encouraged to use one of the binary installers. Experienced users are advised to run the scripts provided by the Coq platform to install from sources as this will allow them to install additional packages with opam. >>
(From https://github.com/coq/platform#installation)

So that's my mistake, it seems. Now looking at https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin

view this post on Zulip Notification Bot (Oct 03 2022 at 17:05):

Lessness has marked this topic as resolved.

view this post on Zulip Lessness (Oct 04 2022 at 17:48):

Success! Now I have opam and have installed coq-hydra-battles. It works.

view this post on Zulip Karl Palmskog (Oct 04 2022 at 18:18):

to build Goedel, you also need coq-coqprime, version dev. See the extra-dev repo here: https://github.com/coq/opam-coq-archive#usage

view this post on Zulip Lessness (Oct 04 2022 at 20:23):

Thank you for your help. Successfully built Goedel. :tada:

view this post on Zulip Notification Bot (Mar 19 2023 at 20:18):

Lessness has marked this topic as resolved.


Last updated: Jun 10 2023 at 23:01 UTC