Michael Soegtrop (Jan 20 2022 at 17:01): Michael Soegtrop (Jan 20 2022 at 17:01):@Jim Fehrle : cause I was busy and there have been a few difficulties the 2021.11 with the latcdebug preview was not really publically relased (but available via Coq Platform main).
Meanwhile we have a Coq Platform 8.15.0 with a reasonable, but not yet complete, Coq Platform preview pick.
Do you think I should keep the latcdebug pick (which has a complete 8.14 pick) or do you think it makes more sense to redirect users to 8.15 preview? The latter might be preferable, because users might installit anyway, so you don't need a long build to play with latcdebug.
Théo Zimmermann (Jan 20 2022 at 17:10):The preview was published in 2021.09 though.
Jim Fehrle (Jan 21 2022 at 03:28):Let's direct them to 8.15.0. At the moment I have nothing to preview beyond that
Michael Soegtrop (Jan 21 2022 at 16:30):@Jim Fehrle : OK. Would you mind to test the 8.15 preview pick in Coq Platform main? This should be pretty close to what will be released next week. I will remove the ltacdebug after your tests.
Jim Fehrle (Jan 21 2022 at 20:05):I can try it Saturday or Sunday. You want me to install the variant and check that the debugger works? Can you give me specific instructions? In WSL or native Windows?
Michael Soegtrop (Jan 22 2022 at 12:06):Essentially you follow these instructions (https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin) except that you use the main branch instead of the 2021.09 tag. At some point it will ask which version you want, and there you pick 8.15~preview1.
Afaik WSL doesn't work easily, because Ocaml 4.10.2 is broken on WSL2 and some Coq Platform components are not compatible with 4.11.
Jim Fehrle (Jan 22 2022 at 18:24):From instructions: "Most users should download and extract https://github.com/coq/platform/archive/refs/tags/2021.09.0.zip." This doesn't show the 8.15 preview, but I think that's expected. (And re-reading your instructions, you must mean I should build from "git clone".)
Jim Fehrle (Jan 22 2022 at 18:24):Also a typo in the script: “The follwoing versions”
Jim Fehrle (Jan 22 2022 at 19:47):I was able to start CoqIDE and do a simple test of the debugger. Anything else you'd like me to check?
Jim Fehrle (Jan 22 2022 at 19:58):A few thoughts:
IIUC each cygwin installation puts files in its own /home directory. Maybe the instructions should mention
a) how to migrate files when you install a new version of the platform, or b) suggest where to
store files outside of Cygwin to avoid the issue.
I had to prefix the .bat files with "./" to run them--maybe you can update the file names in the writeup?
Michael Soegtrop (Jan 23 2022 at 09:15):@Jim Fehrle : thanks for testing - I also did some tests with my stuff, but I am not sure I use all features of the debugger.
Regarding your comments: it all make sense, except that when running the .bat file you are expected to run it from a DOS prompt. But I can add a note that when run from a cygwin shell one should prepend a "./".
Please also note that the docs say (last line of the install instructions) that you can reuse an existing Coq Platform cygwin for another Coq Platform - you just can't reuse any cygwin. So the .bat file you typically run only once per computer. For this reason the home folder issues shouldn't really apply. Is the documentation unclear in this? Maybe I should make the last line first and say "if you already have a Coq Platform Cygwin proceed with step ..."?
Michael Soegtrop (Jan 23 2022 at 13:12):I updated the Readme a bit to distinguish the first / successive install cases.
Btw.: The zip double folder thing comes from Windows / your unzip tool. Usually you have a choice to extract to a folder with the same name as the zip file or to extract here. This is common.
Michael Soegtrop (Jan 23 2022 at 14:45):You can have a look at the updated Windows Readme here:
https://github.com/MSoegtropIMC/platform/blob/msoegtrop/2022.01.prep4/doc/README_Windows.md
Jim Fehrle (Jan 23 2022 at 19:04):when running the .bat file you are expected to run it from a DOS prompt. But I can add a note that when run from a cygwin shell one should prepend a "./".
I don't have git set up to run in a Windows command window, so I have to open a cygwin shell to do the download. Then the natural thing to do is to type the .bat command in the same window rather than open a new window, navigate to the right directory, etc.
Michael Soegtrop (Jan 23 2022 at 19:08):Yes, I just expect that people know that when they run a shell script (or bat file) from the local folder, they need to prepend a "./".
Jim Fehrle (Jan 23 2022 at 19:21):Maybe I should make the last line first and say "if you already have a Coq Platform Cygwin proceed with step ..."?
I stopped following the instructions once I got the platform installed (common user behavior!). This section of the revised instructions uses too many bullet points: some of them are steps to follow while most of them just state facts. I think it would benefit from reorganization and simplification, which I could submit in a PR if you're interested.
Jim Fehrle (Jan 23 2022 at 19:23):I meant "stopped reading the instructions"
Last updated: Jun 03 2023 at 03:01 UTC