Kimaya Bedarkar (Mar 20 2021 at 08:30): 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?
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.
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
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.
Michael Soegtrop (Mar 20 2021 at 09:25):Anyway "Coq Platform" is the frustration free packaging of Coq.
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!
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.
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)
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.
Michael Soegtrop (Mar 20 2021 at 16:17):The require statement for ssreflect should be:
From mathcomp Require Import ssreflect.
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."
Enrico Tassi (Mar 20 2021 at 16:25):Do you happen to have COQLIB set? Could you try export | grep -i coq?
Enrico Tassi (Mar 20 2021 at 16:25):Also, I guess you also run eval $(opam env) right after opam switch, am I right?
Kimaya Bedarkar (Mar 20 2021 at 16:26):Enrico Tassi said:
Also, I guess you also run
eval $(opam env)right afteropam switch, am I right?
Yeah I did this
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?
Christian Doczkal (Mar 20 2021 at 16:35):You run the suggested command: export | grep -i coq.
Christian Doczkal (Mar 20 2021 at 16:37):(Normally, that should not generate any output)
Michael Soegtrop (Mar 20 2021 at 16:38):I guess I should check this in the platform scripts and warn about it.
Michael Soegtrop (Mar 20 2021 at 16:40):As is this doesn't seem to be entirely "frustration free" as I advertised ...
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
Enrico Tassi (Mar 20 2021 at 16:53):you can unset COQLIB then, it may be the cause of your troubles
Enrico Tassi (Mar 20 2021 at 16:53):assuming COQLIB=..... is part of the output
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
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.
Kimaya Bedarkar (Mar 20 2021 at 17:16):Christian Doczkal said:
Well, the
exportshould generate some output, but the| grep -i coqis 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
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...
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.
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...
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
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
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.
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.
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.
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).
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)
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")
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 ;-)
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".
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?
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.
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)
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).
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:
all_ssreflect, but it also "cheat" here and there disabling some notations (to present things one at a time, while by loading all_ssreflect you geteverything). ssreflect and ssrbool (from mathcomp even if not is it strictly necessary), but then anyway, at page 16, as soon as it starts to talk about recursive programs, it loads ssrnat which is not in plain Coq.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:
Search) rewrite behind the scenese, and having the plugin part of Coq makes their life simpler 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.
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.
Kimaya Bedarkar (Mar 24 2021 at 05:05):Thank you everyone for your help! I have started learning ssreflect now!
Last updated: Oct 13 2024 at 01:02 UTC