Stream: Coq users

Topic: Trouble installing ssreflect


view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 08:30):

Hello!
I am trying to learn how to use ssreflect. I am trying to install it on my machine but I seem to be hitting the same error whatever I try. I installed coq using opam and tried installing ssreflect using the opam commands given but it returns the error : "Sorry, no solution found: there seems to be a problem with your request.No solution found, exiting". Could someone help me please?

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:11):

You likely have some opam packages pinned to a version which is incompatible with any version of ssreflect. You might want to try the scripts here : (https://github.com/coq/platform). These script will create a fresh opam switch and install Coq, ssreflect and a few other things from opam. The readme also gives a list of package versions which do work together.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:15):

With "fresh opam switch" I mean that it doesn't touch whatever you already have in opam. You can switch any time between the new switch and your current opam switch - it takes a fraction of a second. See opam switch --help

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:23):

Thinking about it: in modern Coq (since 8.12?) ssreflect is included in plain Coq. So your problem might be that opam says it can't install ssreflect because it is already installed as part of coq.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 09:25):

Anyway "Coq Platform" is the frustration free packaging of Coq.

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 09:26):

I don't think the issue is that it is already installed because, when i try importing the libraries in the code it's giving me an error. I will try Coq Platform. Thanks!

view this post on Zulip Enrico Tassi (Mar 20 2021 at 09:48):

Indeed, use the platform. There once used to be a package called coq-ssreflect which depends on an ancient Coq. Today it is called coq-mathcomp-ssreflect, maybe that was your problem. If you found instructions using that package name, please tell me where, so that I can erase them.

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 15:37):

Michael Soegtrop said:

With "fresh opam switch" I mean that it doesn't touch whatever you already have in opam. You can switch any time between the new switch and your current opam switch - it takes a fraction of a second. See opam switch --help

I am not sure I understand how switches work. I installed the coq-platform using snap but it still gives me error when I import ssreflect from mathcomp. I am not sure what I am getting wrong. How do I know I am accessing the right opam switch when I start writing code in the ide.

(sorry if my doubts are too naive, I am just getting started with writing some code)

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 16:14):

I must admit I am not sure how this works with the snap package - I expect that this does not install opam or an opam switch, but a working Coq system. @Enrico Tassi is the expert here.

What I referred to is downloading the Coq platform scripts and running them (which will take on hour or so).

The Coq platform offers two different installation methods: compile from sources using opam (this will create an opam switch) and install a binary delivery (at least on Windows and Mac this uses opam to create the installer, but the installed artifacts don't include opam or a switch). If you are already familiar with opam, the script based "compile from sources" variant might be more what you want.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 16:17):

The require statement for ssreflect should be:

From mathcomp Require Import ssreflect.

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 16:22):

Ah I see. I got that later so I installed using the first method. It created the switch and I used "opam switch _coq-platform_.2021.02.0" before launching coqide from the terminal. Then I used the command suggested above. I still get this error in coqide : "Cannot find a physical path bound to logical path matching suffix <> and prefix mathcomp."

view this post on Zulip Enrico Tassi (Mar 20 2021 at 16:25):

Do you happen to have COQLIB set? Could you try export | grep -i coq?

view this post on Zulip Enrico Tassi (Mar 20 2021 at 16:25):

Also, I guess you also run eval $(opam env) right after opam switch, am I right?

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 16:26):

Enrico Tassi said:

Also, I guess you also run eval $(opam env) right after opam switch, am I right?

Yeah I did this

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 16:33):

Enrico Tassi said:

Do you happen to have COQLIB set? Could you try export | grep -i coq?

How exactly do I check if i have COQLIB set?

view this post on Zulip Christian Doczkal (Mar 20 2021 at 16:35):

You run the suggested command: export | grep -i coq.

view this post on Zulip Christian Doczkal (Mar 20 2021 at 16:37):

(Normally, that should not generate any output)

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 16:38):

I guess I should check this in the platform scripts and warn about it.

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 16:40):

As is this doesn't seem to be entirely "frustration free" as I advertised ...

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 16:47):

Christian Doczkal said:

(Normally, that should not generate any output)

Ah. It is generating some output for me

view this post on Zulip Enrico Tassi (Mar 20 2021 at 16:53):

you can unset COQLIB then, it may be the cause of your troubles

view this post on Zulip Enrico Tassi (Mar 20 2021 at 16:53):

assuming COQLIB=..... is part of the output

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 16:56):

Enrico Tassi said:

assuming COQLIB=..... is part of the output

Its not. I get stuff like
declare -x CAML_LD_LIBRARY_PATH="....." etc

view this post on Zulip Christian Doczkal (Mar 20 2021 at 17:08):

Well, the export should generate some output, but the | grep -i coq is supposed to filter everything not relevant to Coq.

view this post on Zulip Kimaya Bedarkar (Mar 20 2021 at 17:16):

Christian Doczkal said:

Well, the export should generate some output, but the | grep -i coq is supposed to filter everything not relevant to Coq.

it didn't filter out these because "_coq-platform_.2021.02.0" is part of the PATH

view this post on Zulip Enrico Tassi (Mar 20 2021 at 17:48):

Hum, another way to debug this woud be the run, in Coq, Print LoadPath. and see what it prints. It should print stuff in ~/.opam/_coq-platform...

view this post on Zulip Michael Soegtrop (Mar 20 2021 at 21:17):

@Kimaya Bedarkar : if you find out what it is, please let me know. I can add sanity checks to the coq platform scripts to exclude this issue in the future.

view this post on Zulip Théo Zimmermann (Mar 20 2021 at 21:56):

Sometimes, the issue is that there are several versions of Coq installed on a system and the one that is picked when running CoqIDE is not the one that has ssreflect installed...

view this post on Zulip Kimaya Bedarkar (Mar 21 2021 at 06:03):

Michael Soegtrop said:

Kimaya Bedarkar : if you find out what it is, please let me know. I can add sanity checks to the coq platform scripts to exclude this issue in the future.

yeah sure

view this post on Zulip Kimaya Bedarkar (Mar 21 2021 at 06:04):

Théo Zimmermann said:

Sometimes, the issue is that there are several versions of Coq installed on a system and the one that is picked when running CoqIDE is not the one that has ssreflect installed...

Yeah I also thought this might be the issue so I launched coqide from the terminal after using opam switch

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 06:37):

@Kimaya Bedarkar : if you can't get it fixed, let's have a quick remote desktop session. This is probably most efficient for both of us. Just send me a private message when you have time - I am mostly available today.

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 12:40):

FTR: @Kimaya Bedarkar just installed Coq+CoqIDE with Coq platform - probably my fault because I said above ssreflect is included in Coq.

@Enrico Tassi : actually I am quite confused about this. Can you elaborate a bit on the question what is included with Coq and what not? I thought that ssreflect itself is included in Coq and coq-mathcomp-ssreflect is an extension of ssreflect for mathcomp.

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:26):

If I'm not mistaken, the recent history is: initially there was just "ssreflect" which was a plugin and a library (opam coq-ssreflect), then there was a split (the plugin and some basic libraries and mathcomp, opam coq-mathcomp-ssreflect and coq-mathcomp-*), then the plugin was merged in Coq together with 3 files from coq-mathcomp-ssrereflect, which still exists since that mathcomp component is around 15 files, so it did not get empty when "ssreflect" (the proof language) was merged into Coq.

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:28):

Coq ships ssreflect ssrfun ssrbool (and ssrmatching, which was made a separate plugin and merged into Coq even before ssreflect was).

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:30):

While coq-mathcomp-ssreflect ships bigop binomial choice div eqtype fingraph finset fintype generic_quotient order path prime seq ssrAC ssrnat ssrnotations tuple (plus some backward compat proxies for ssrfun, ssrbool and ssreflect)

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:33):

To conclude today "ssreflect" means only 2 things (instead of 3): the proof language (in Coq) and the first component of mathcomp that provides some data structures and some discrete mathematics (it is by far the most widely used mathcomp component, since it is also pretty relevant for computer science, not just "math")

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:35):

Actually, "ssreflect" is also a formalization style (small scale reflection, aka boolean reflection), which is well supported by the proof language and one of the key ingredients of mathcomp. But al least that is not something you "install", so it should not be the cause of confusion ;-)

view this post on Zulip Enrico Tassi (Mar 21 2021 at 13:43):

FTR: the platform 2021.02.x ships all which can be referred to as "ssreflect" or "mathcomp".

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 14:20):

Im still not sure what the difference between these two is:

From mathcomp Require Import ssreflect.

Require Import ssreflect.

Does the first refer to the second or does it duplicate things or is this something entirely different?

view this post on Zulip Enrico Tassi (Mar 21 2021 at 14:29):

Yes, the one from mathcomp loads the one from Coq. From time to time we put in the mathcomp one some extra stuff while we "backport" that to Coq.

view this post on Zulip Enrico Tassi (Mar 21 2021 at 14:32):

Note that for each component mathcomp provides a From mathcomp Require Import all_component, eg all_ssreflect which loads all files in the right order and from the right place. That should be the preferred way to load the ssreflect component from mathcomp (unless you have good reasons for leaving some files out)

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 17:09):

@Enrico Tassi : thanks for the clarification!

Coming back to the original question from @Kimaya Bedarkar : would it have been reasonable to advise her for the goal of learning ssreflect to just do "Require Import ssreflect" or should one always use the one from mathcomp unless one has a good reason for not doing so (other than the difficulty to get it installed).

view this post on Zulip Enrico Tassi (Mar 21 2021 at 17:43):

That is not an easy question. To use ssr, I'd recommend all_ssreflect from mathcomp.
To learn ssr it depends on the textbook:

To sum up, the files in Coq give you a fully functional proof language and enough theory to do propositional (classical) logic exercises, but nothing more. So I would recommend installing coq-mathcomp-ssreflect anyway, and depending on the textbook, load what it suggests.

It is still interesting to have the ssreflect plugin in Coq:

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 17:50):

Thanks! So I guess one shouldn't state towards non-expert users that ssreflect is part of Coq (as I did). It seems to be an information which is more relevant to advanced users and otherwise more confuses than helps.

view this post on Zulip Enrico Tassi (Mar 21 2021 at 17:58):

I guess so, but I would also ask what they mean by "learning ssreflect", because it may be that they really want to learn mathcomp instead, or just want to find the reference manual of the ssr proof language (which is inside the Coq manual). Unfortunately the term "ssreflect" is still quite overloaded, as far as I can tell.

view this post on Zulip Kimaya Bedarkar (Mar 24 2021 at 05:05):

Thank you everyone for your help! I have started learning ssreflect now!


Last updated: Jan 31 2023 at 14:03 UTC