Stream: Coq users

Topic: ✔ Problem installing HighSchoolGeometry on Ubuntu


view this post on Zulip Julio Di Egidio (Nov 24 2023 at 17:46):

Hi guys, trying to work with coq-community/HighSchoolGeometry, I have:

Then, as per instructions on the project readme, I have:

julio@CoqUbuntu01:~/Desktop/WORK/HighSchoolGeometry$ make install
make[1]: Entering directory '/home/julio/Desktop/WORK/HighSchoolGeometry'
install: cannot change permissions of ‘/snap/coq-prover/33/coq-platform/lib/coq//user-contrib/HighSchoolGeometry/’: No such file or directory
...several more lines identical to the one above...
make[1]: *** [Makefile.coq:613: install] Error 1
make[1]: Leaving directory '/home/julio/Desktop/WORK/HighSchoolGeometry'
make: *** [Makefile:14: install] Error 2

Should I fix it somehow? (I can already work with .v files in CoqIDE.)

Thanks for any advice.

cc: @Karl Palmskog

view this post on Zulip Huỳnh Trần Khanh (Nov 24 2023 at 17:46):

you usually don't need to do make install

view this post on Zulip Karl Palmskog (Nov 24 2023 at 17:47):

right, the Snap is not really meant for people who want to install new Coq libraries, then one should use the Platform installation scripts.

view this post on Zulip Karl Palmskog (Nov 24 2023 at 17:48):

and it's not really necessary to install a Coq project unless there is some other project that depends on it (not the case with HighSchoolGeometry)

view this post on Zulip Julio Di Egidio (Nov 24 2023 at 17:49):

OK, so I gather I am already good to go. Thank you both.

view this post on Zulip Notification Bot (Nov 24 2023 at 17:49):

Huỳnh Trần Khanh has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (Nov 25 2023 at 08:02):

@Julio Di Egidio : technically the snap is a read only image file system, and the coq library folder lives in this read only file system, so one can't install anything in it, even not with sudo.


Last updated: Jun 23 2024 at 04:03 UTC