Matthieu Sozeau (Mar 12 2021 at 10:04): Matthieu Sozeau (Mar 12 2021 at 10:04):I'm wondering if we could make coq-hott available in the platform: we're doing a HoTT-related summer school next month that could benefit from it. @Michael Soegtrop or @Enrico Tassi was there any issue with including it? (Maybe on windows it's not so easy)
Emilio Jesús Gallego Arias (Mar 12 2021 at 10:13):@Matthieu Sozeau TTOMK it should be fine
Théo Zimmermann (Mar 12 2021 at 11:42):@Matthieu Sozeau There's already an issue tracking that: https://github.com/coq/platform/issues/7
A summary of the situation:
Notification Bot (Mar 12 2021 at 11:42):This topic was moved here from #Coq devs & plugin devs > Coq-HoTT in the platform? by Théo Zimmermann
Ali Caglayan (Mar 12 2021 at 11:43):I've been working on getting rid of the custom hoq stuff, but I was waiting for changes in coq and dune.
Ali Caglayan (Mar 12 2021 at 11:44):Our current makefile set up does much more than build the library (documentation, proviola etc.)
Ali Caglayan (Mar 12 2021 at 11:44):It should be possible to get rid of most of this now, but I haven't had the time recently
Ali Caglayan (Mar 12 2021 at 11:45):There is some work that needs to be done in the HoTT library to completely severe it from the coq stdlib.
Bas Spitters (Mar 12 2021 at 12:07):@Michael Soegtrop has created a version of the windows installer before for an earlier HoTT workshop.
Enrico Tassi (Mar 12 2021 at 13:13):CI is building it at every run, if you fork the repo and change the list of opam packages you get one
Enrico Tassi (Mar 12 2021 at 13:14):About adding it officially, 2021.02.1 ws about the OSX installer, 2021.02.2+ for adding packages, so it is not planned before the OSX isntaller is fixed
Michael Soegtrop (Mar 13 2021 at 12:55):so it is not planned before the OSX isntaller is fixed
I am working on this right now ...
How is the installation structure of HoTT now? Back then one needed a different standard library and things where pretty incompatible. Afair the solution back then was to create scripts for the major executables, which setup things so that coqc would pick up the correct files. Would this still be required?
Ali Caglayan (Mar 13 2021 at 12:55):Technically this is still required, but with the splitting of coq-core it should be much easier to handle now. I just haven't had time to do this yet.
Ali Caglayan (Mar 13 2021 at 12:56):In order words, nothing much has changed
Bas Spitters (Mar 13 2021 at 13:16):https://github.com/HoTT/HoTT/issues/1424
Michael Soegtrop (Mar 14 2021 at 17:01):So you ping me, when you are ready? Otherwise it likely wouldn't be hard to make a Coq platform variant for HoTT. I anyway want to put all Coq versions into one Coq Platform branch, so that there is only one package file per Coq version and all the rest is shared. One could easily add a HoTT variant.
Michael Soegtrop (Mar 28 2021 at 09:30):@Bas Spitters : in the license thread you mentioned that you have an upcomming HoTT school. Do you think it makes sense to make a HoTT specialization of Coq Platform now?
I anyway wanted to change the Coq Platform such that it can build different versions of Coq platform and would ask at startup which version you want. One could add a HoTT version there.
But I would need some background info on how to build it / set it up. Maybe a conf call on the topic would help.
Bas Spitters (Mar 28 2021 at 09:32):@Matthieu Sozeau has been preparing an image for the students. I'm not entirely sure what the status is.
Michael Soegtrop (Mar 28 2021 at 10:25):@Matthieu Sozeau : is this Coq platform based or does it work in a different way?
Matthieu Sozeau (Mar 29 2021 at 14:37):I'm a bit behind, I didn't start yet, so yes a conference call at your earliest convenience would be great!
Matthieu Sozeau (Mar 29 2021 at 14:43):Otherwise if you could point me to where the specialization should happen I can give it a try. Right now the coq-hott opam package installs its own hoqtop/hoqidetop, so already just being able to have this package would suffice. I mean we don't need to do anything special about it.
Matthieu Sozeau (Mar 29 2021 at 14:46):I'll try just following the README instructions on a custom installer and report :)
Enrico Tassi (Mar 29 2021 at 15:22):if you open a (draft) PR against coq/platform you will get CI build all the stuff for you.
Matthieu Sozeau (Mar 29 2021 at 15:39):Yes, I'm trying that
Michael Soegtrop (Mar 29 2021 at 15:54):@Matthieu Sozeau : if you have time now, we can have a chat on this.
Matthieu Sozeau (Mar 29 2021 at 15:55):I'm in a meeting, but maybe in about ~1hr?
Enrico Tassi (Mar 29 2021 at 15:56):@Michael Soegtrop see also the PR https://github.com/coq/platform/pull/97 , I left some comment there, but a skype will surely go faster ;-)
Michael Soegtrop (Mar 29 2021 at 15:58):@Enrico Tassi : are you also available around 7 PM?
Enrico Tassi (Mar 29 2021 at 15:58):nope
Michael Soegtrop (Mar 29 2021 at 15:59):OK, then I try to sort it out with Matthieu. I would first do a branch for this and later merge it together with the changes to make the platform multi target (Coq 8.13, 8.12, 8.11 ...).
Matthieu Sozeau (Mar 29 2021 at 16:31):I'm available now @Michael Soegtrop
Michael Soegtrop (Mar 29 2021 at 17:08):@Matthieu, sorry I didn't see your message here (email works better) I send you an invite.
Michael Soegtrop (Mar 29 2021 at 18:04):@Enrico Tassi : I had a discussion with @Matthieu Sozeau . Currently HoTT uses scripts to start Coq which is not that appsopriate if we anyway generate a separate switch for it. Di you think one could extend the coq_environment.txt mechanism such that one could also give command line arguments in there? Most important would be -indices-matter. It also gives a few -R and -Q options, but I don't think one needs this of paths are set up properly.
Mid term one could think about having a command line argument and/or environment variable to switch environment files, so that one can easily switch between HoTT and normal Coq.
What do you think? Does it make sense?
Matthieu Sozeau (Mar 29 2021 at 18:43):The CI worked! https://github.com/coq/platform/pull/97/checks?check_run_id=2220877237
Matthieu Sozeau (Mar 29 2021 at 18:47):I'm going to test them.. If only I could get the MacOS package as well that would be great!
Enrico Tassi (Mar 29 2021 at 19:38):just rebase on top of https://github.com/coq/platform/pull/50
Michael Soegtrop (Mar 29 2021 at 22:28):@Matthieu Sozeau : the smoke test looks fishy, though - it includes all packages. Didn't you disable most packages?
Matthieu Sozeau (Mar 29 2021 at 22:33):It includes VST and compcert, which I thought could be disabled using PLATFORM_ARGS: -extent=f -parallel=p -jobs=2 -vst=n -compcert=n
in the CI script but that didn't do it
Matthieu Sozeau (Mar 29 2021 at 22:35):Indeed I have them available in the OS X package I'm testing now
Matthieu Sozeau (Mar 29 2021 at 22:37):Ah that changed with my rebase on #50, that might be it
Matthieu Sozeau (Mar 29 2021 at 22:42):I'll need to run a script on the hoq-config file that is installed by the coq-hott package, so that it can relocate into /Applications/... apparently
Matthieu Sozeau (Mar 29 2021 at 22:43):Otherwise everythings there and can be run (with a little bit of path fiddling)
Michael Soegtrop (Mar 30 2021 at 06:40):On Mac you can run such a script before creating the DMG installer (rather than asking the user to do it afte rinstall) since one can assume that the installation is always under /Applications.
Michael Soegtrop (Mar 30 2021 at 06:40):So what is left to do? Test it on Mac and Windows?
Matthieu Sozeau (Mar 30 2021 at 08:59):Yes. I need to find where to run the script to change hoq-config for all versions, and test it :)
Matthieu Sozeau (Mar 30 2021 at 09:02):Also, on MacOS, the installer missed a symlink that should be installed as well
Matthieu Sozeau (Mar 30 2021 at 09:03):I guess it should be changed in create_installer_macos.sh
Matthieu Sozeau (Mar 30 2021 at 09:11):Can I assume we have gnu sed installed?
Enrico Tassi (Mar 30 2021 at 09:13):you should check for it in the script https://github.com/coq/platform/pull/50/files#diff-0c76aa735af08df2c485e007971414f552bee2cb028351c44b2c0ccea457fa96R45, and install it here https://github.com/coq/platform/pull/50/files#diff-7b74d73de878e0e53f6768bbf3a3d4b50c3c6f1f16f9b64518690028b8206b1cR84
Guillaume Melquiond (Mar 30 2021 at 09:18):Be careful. If I remember correctly, brew installs sed as gsed.
Enrico Tassi (Mar 30 2021 at 09:40):I believe both brew and ports call it gsed
Enrico Tassi (Mar 30 2021 at 09:40):(which is good, since the dmg script is expected to run on OSX only, so we can just ditch "sed")
Matthieu Sozeau (Mar 30 2021 at 09:45):Yep, I'm using gsed all the time :)
Michael Soegtrop (Mar 30 2021 at 10:01):If you need help with translating - please let me know ;-)
Btw.: awk tends to be more compatible and is anyway easier to read for non trivial stuff.
Matthieu Sozeau (Mar 30 2021 at 10:08):It's just a path change, I think that'll be fine
Matthieu Sozeau (Mar 30 2021 at 10:08):I think I've got macos covered, now about windows and the snap package
Matthieu Sozeau (Mar 30 2021 at 10:09):Did you manage to try a build for windows @Michael Soegtrop ?
Ali Caglayan (Mar 30 2021 at 10:13):Just to let you guys know, I am currently getting rid of the hoq stuff. We have already removed our version of the coq prelude so we just need to change some makefiles at the moment.
Michael Soegtrop (Mar 30 2021 at 10:18):Matthieu Sozeau said:
Did you manage to try a build for windows Michael Soegtrop ?
I started the build but didn't look at the results as yet ...
Matthieu Sozeau (Mar 30 2021 at 10:18):That's nice, it should be easy to change the script to not do the fixes if we get there in the next two weeks
Michael Soegtrop (Mar 30 2021 at 10:21):@Ali Caglayan : that is great news! So in a near future one can add HoTT as package to the Coq Platform and just Require Include HoTT.HoTT. and it will work?
Ali Caglayan (Mar 30 2021 at 10:32):That should work. I am currently experimenting with coq_makefile and it seems to be working. HoTT obviously needs the -noinit and -indices-matter flags however so I am not sure you can just import it into any file.
Théo Zimmermann (Mar 30 2021 at 10:34):I guess you could as long as you have a _CoqProject file that contains: -arg -noinit -arg -indices-matter
Michael Soegtrop (Mar 30 2021 at 10:36):@Théo Zimmermann : that should be substantially more convenient than using hoqc, especially since one can include such a _CoqProject file in any relevant project.
Ali Caglayan (Mar 30 2021 at 11:15):Yeah, so this works fine. The main issue I am currently having is replacing our current makefile set up to call the coq makefile thing instead. However our current makefile does so much and is so intertwined with custom targets that I am having trouble separating things.
Ali Caglayan (Mar 30 2021 at 11:15):https://github.com/HoTT/HoTT/pull/1431
Ali Caglayan (Mar 30 2021 at 11:16):I've changed the _CoqProject so that we can now build the HoTT library with coq_makefile
Ali Caglayan (Mar 30 2021 at 11:16):If you want to make an installer for coq platform you should be able to now, just do the usual:
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile
I have a question about the makefile set up however. It seems that messages are printed into the make output. I know I have observed this before with @Emilio Jesús Gallego Arias when working on a dune set up. AFAIK there is a way to mute this in the makefile version, how is this done?
Matthieu Sozeau (Mar 30 2021 at 11:26):You mean the VERBOSE=1 (V=1 in HoTT Makefiles I think)?
Ali Caglayan (Mar 30 2021 at 11:28):What's happening is the following in the output:
COQC theories/Equiv/Relational.v
COQC theories/PropResizing/PropResizing.v
COQC theories/Metatheory/FunextVarieties.v
NaiveFunext
: Type
NaiveNondepFunext
: Type
WeakFunext
: Type
COQC theories/Categories/Category/Morphisms.v
due to Print statements in some files.
Guillaume Melquiond (Mar 30 2021 at 11:29):Is there a reason to keep these Print statements in the first place?
Ali Caglayan (Mar 30 2021 at 11:30):sometimes there is a Check also
Ali Caglayan (Mar 30 2021 at 11:30):especially in the unit tests
Guillaume Melquiond (Mar 30 2021 at 11:32):I am not sure to understand. What is the point of having Check in a unit test if you do not test the output of Check? If it is just to check that a term has a given type, you could just as well use Definition.
Gaëtan Gilbert (Mar 30 2021 at 11:32):but then you have to give a name to definition
and fill any evars
Ali Caglayan (Mar 30 2021 at 11:35):I think when I spoke with Emilio about this a while back, we agreed that the current message passing system is not ideal.
Matthieu Sozeau (Mar 30 2021 at 11:36):We should rather put Definition foo : expected_type := test in the test-suite files, or really do output tests like we do in Coq's test-suite
Guillaume Melquiond (Mar 30 2021 at 11:37):No, the output of Check goes to stdout.
Emilio Jesús Gallego Arias (Mar 30 2021 at 11:56):Indeed I have a PR which I did wit Ali , I hope to finish it up and submit, we agreed that there we some problems with the current system, it is a long story on how messages have been handled by Coq.
Michael Soegtrop (Mar 30 2021 at 12:00):Regarding the prints: if this is built as a package with opam, opam will anyway redirect the output to a log file. There are other packages which produce (a lot) of output. So from a point of understandability of Coq Platform CI output, it doesn't matter a lot (it matters, but not a lot).
Matthieu Sozeau (Mar 30 2021 at 14:31):@Ali Caglayan would you happen to use Linux and could test the platform snap package for Coq + HoTT ?
Ali Caglayan (Mar 30 2021 at 14:32):@Matthieu Sozeau I am using linux and I would be able to test
Ali Caglayan (Mar 30 2021 at 14:32):What should I do?
Matthieu Sozeau (Mar 30 2021 at 14:32):Cool, it's here: https://github.com/coq/platform/actions/runs/701471850
Matthieu Sozeau (Mar 30 2021 at 14:34):A priori, you install it, and follow the instructions there: https://github.com/HoTT/EPIT-2020/pull/2/files
Matthieu Sozeau (Mar 30 2021 at 14:34):I don't know snap though :)
Ali Caglayan (Mar 30 2021 at 14:37):it still looks like you are using hoq scripts, you shouldn't need to after the PR i submitted is done.
Ali Caglayan (Mar 30 2021 at 14:39):I don't see any instructions for snap there btw
Ali Caglayan (Mar 30 2021 at 14:39):but I am doing it the usual snap way
Matthieu Sozeau (Mar 30 2021 at 14:43):Indeed, you still need to find hoqidetop, but that should disappear (not exactly sure though because I'm not sure we can pass arbitrary options in CoqIDE)
Enrico Tassi (Mar 30 2021 at 14:45):Matthieu Sozeau said:
I don't know snap though :)
Here it is: sudo snap install --dangerous xxxx_amd64.snap
Enrico Tassi (Mar 30 2021 at 14:46):I can try it out for you
Ali Caglayan (Mar 30 2021 at 14:46):Something is wrong with my snap:
error: cannot communicate with server: Post http://localhost/v2/snaps: dial unix /run/snapd.socket: connect: no such file or directory
It also hangs when I write snap --version
Ali Caglayan (Mar 30 2021 at 14:47):That doesn't look healthy
Enrico Tassi (Mar 30 2021 at 14:49):do you have snapd running? which linux distro are you on?
Ali Caglayan (Mar 30 2021 at 14:50):I didn't know we have to have snapd running?
Ali Caglayan (Mar 30 2021 at 14:50):I am using ubuntu bionic
Ali Caglayan (Mar 30 2021 at 14:50):I just installed snapd from ubuntu repos
Enrico Tassi (Mar 30 2021 at 14:50):it install fine here, but it does not include HoTT
Matthieu Sozeau (Mar 30 2021 at 14:52):That's curious :)
Enrico Tassi (Mar 30 2021 at 14:53):the snap by default has reduced platform args, change them (temporarily) in your PR by editing snap.yaml
Matthieu Sozeau (Mar 30 2021 at 14:53):Yep, I'll have a look
Enrico Tassi (Mar 30 2021 at 14:53):zap -extent=i
Matthieu Sozeau (Mar 30 2021 at 14:54):I just put extent=f ?
Matthieu Sozeau (Mar 30 2021 at 14:58):Let's try
Matthieu Sozeau (Mar 30 2021 at 15:29):New snap package here: https://github.com/coq/platform/actions/runs/701849310
Matthieu Sozeau (Mar 30 2021 at 15:29):With HoTT this time :)
Michael Soegtrop (Mar 30 2021 at 15:38):@Matthieu Sozeau : I guess you tested this already on Mac, so what is left is testing on Windows?
Matthieu Sozeau (Mar 30 2021 at 15:39):@Enrico Tassi @Michael Soegtrop would it be ok to distribute the packages on github as a specific 2021.02-hott platform release when they're ready?
Matthieu Sozeau (Mar 30 2021 at 15:39):Yes, it's all that's left
Michael Soegtrop (Mar 30 2021 at 15:41):(After install you have to right click on the app and say open, then you get an "unsigned warning" message box, where you can decide to "run anyway")
Michael Soegtrop (Mar 30 2021 at 15:41):@Enrico Tassi : any chance we get this signed by INRIA?
Matthieu Sozeau (Mar 30 2021 at 15:42):Yep, it's the same with the MacOS version, that reminds me I should warn users about it
Matthieu Sozeau (Mar 30 2021 at 15:43):If we can get them signed that would be great indeed
Enrico Tassi (Mar 30 2021 at 15:53):for macos we can sign it by ourselves (not notarize it, which even Inria cannot)
Enrico Tassi (Mar 30 2021 at 15:53):Here the howto: https://github.com/coq/coq/wiki/SigningReleases
Enrico Tassi (Mar 30 2021 at 15:54):you need to access the osx slave, you both have the right I believe
Enrico Tassi (Mar 30 2021 at 15:54):but you need the certificate password, I can give you that in a private chat
Enrico Tassi (Mar 30 2021 at 15:55):do you want to follow the procedure? (cause I've to go)
Matthieu Sozeau (Mar 30 2021 at 15:56):Sure
Matthieu Sozeau (Mar 30 2021 at 15:57):Thanks !
Michael Soegtrop (Mar 30 2021 at 16:10):Cool! Notarization is currently optional (even on BigSur afaik). Also afaik anybody with an Apple developer account can do it. One just uploads the signed app to Apple, they check it for viruses / malware and sign it with an Apple signature that they checked it. Afaik this is free of charge.
Matthieu Sozeau (Mar 30 2021 at 16:11):Would you happen to have an apple dev account ? :)
Matthieu Sozeau (Mar 30 2021 at 16:20):Notarization requires a bit of work it seems, but nothing impossible
Matthieu Sozeau (Mar 30 2021 at 16:21):Hmm, ci.inria.fr seems really unstable...
Théo Zimmermann (Mar 30 2021 at 16:37):If HoTT is ready to properly package in the Coq Platform (in particular without hoq and hoqide) and the macOS installer is also ready, what about just releasing 2021.02.1 in time for the spring school with HoTT included inside?
Théo Zimmermann (Mar 30 2021 at 16:37):It looks like it would bring less confusion and be better for everyone.
Matthieu Sozeau (Mar 30 2021 at 16:58):That would be simpler indeed. I'm for it.
Michael Soegtrop (Mar 30 2021 at 17:02):I am currently looking at the Windows installer created by CI. It installs something but I have no idea how the scripts are supposed to work on Windows. Theres is neiter a Posix shell nor the concept of executable scripts.
Michael Soegtrop (Mar 30 2021 at 17:04):For console calls one can up to a certain extent use batch files, but it would be better to replace the shell scripts with small C files.
Michael Soegtrop (Mar 30 2021 at 17:05):Does someone know how hoqidetop is started by CoqIDE?
Ali Caglayan (Mar 30 2021 at 17:07):Atm there is a script hoqide
Ali Caglayan (Mar 30 2021 at 17:08):but if you wait a little bit https://github.com/HoTT/HoTT/pull/1431 will allow for use of coqide
Michael Soegtrop (Mar 30 2021 at 17:08):Not that I can see it ... Anyway a shell script won't work on Windows.
Michael Soegtrop (Mar 30 2021 at 17:08):What might work is do the argument hacking with a _CoqProject file, as Théo suggested.
Ali Caglayan (Mar 30 2021 at 17:08):ah then its probably generated by ./autogen.sh
Michael Soegtrop (Mar 30 2021 at 17:09):But is it shell script or a batch file? Shell scripts are of no use. All the other files like hoqc are posix shell scripts.
Michael Soegtrop (Mar 30 2021 at 17:10):How can I test if HoTT works? Can someone point me to a not entirely trivial tets file?
Matthieu Sozeau (Mar 30 2021 at 17:10):@Michael Soegtrop in principle you can just start coqide -coqlib .../share/hott/coq -R .../share/hott/theories HoTT -indices-matter
Ali Caglayan (Mar 30 2021 at 17:10):Require Import HoTT.Basics.
Check Contr.
Here is one: https://github.com/HoTT/EPIT-2020/pull/2/files#diff-3110edd8b78b8e325fdeee6f017dd26ca7a2a3a5ca318427a34477e52ee7c6b3
Michael Soegtrop (Mar 30 2021 at 17:11):OK, then I think we should provide a _CoqProject file for users which sets these arguments
Michael Soegtrop (Mar 30 2021 at 17:11):Let me try the _CoqProject approach ...
Matthieu Sozeau (Mar 30 2021 at 17:11):Ah, I didn't think of that, indeed that's good!
Ali Caglayan (Mar 30 2021 at 17:11):This is exactly what https://github.com/HoTT/HoTT/pull/1431 does
Ali Caglayan (Mar 30 2021 at 17:12):This hasn't been merged yet since I wrote it today, but I can speed that a long a bit
Michael Soegtrop (Mar 30 2021 at 17:12):@Ali Caglayan : there are two different things, a _CoqProject file for building HoTT and one for users so that HoTT is properly imported.
Matthieu Sozeau (Mar 30 2021 at 17:13):Indeed, but it can also be used by the user itself, your _CoqProject only applies in the HoTT library
Ali Caglayan (Mar 30 2021 at 17:13):Ah I see what you mean now
Michael Soegtrop (Mar 30 2021 at 17:13):I think one can get around all the hoqxyz files with a simple _CoqProject file.
Michael Soegtrop (Mar 30 2021 at 17:14):Give me a few minutes ...
Matthieu Sozeau (Mar 30 2021 at 17:15):In principle yes, as long as coqide/coqtop is in the path and the IDEs pick the _CoqProject up (I think all do), we just have to instruct the users to put this configuration file at the root of their project. But it will still have to have the weird share/ paths until we update to use Ali's PRs
Michael Soegtrop (Mar 30 2021 at 17:22):@Matthieu Sozeau : the ... in the path are supposed to refer to the Coq root folder?
Michael Soegtrop (Mar 30 2021 at 17:24):This doesn't seem to work.
Michael Soegtrop (Mar 30 2021 at 17:27):Absolute paths do work, though, both on the command line and in a _CoqProject file. So one could supply a batch file which creates a suitable _CoqProject file for HoTT.
Michael Soegtrop (Mar 30 2021 at 17:28):This _CoqProject file works for me:
-R T:\test\CoqPlatform_2021_02_0_HoTT/share/hott/theories HoTT
-arg -coqlib
-arg T:\test\CoqPlatform_2021_02_0_HoTT/share/hott/coq
-arg -indices-matter
If I start coqide without options and load a file Test.v with contents:
Require Import HoTT.Basics.
Check Contr.
it runs through.
Matthieu Sozeau (Mar 30 2021 at 17:28):Yes, I was refering to the absolute paths
Matthieu Sozeau (Mar 30 2021 at 17:28):Great!
Michael Soegtrop (Mar 30 2021 at 17:29):Ah OK, I thought there was some magic in Coq to interpret ... as Coq root (which would be a super cool feature btw.)
Matthieu Sozeau (Mar 30 2021 at 17:29):Now if we have Ali's PRs, coq can find the HoTT library itself (as it'll be in coq/user-contrib)
Michael Soegtrop (Mar 30 2021 at 17:30):But we still need the Coqlib option and -indices-matter or not?
Matthieu Sozeau (Mar 30 2021 at 17:30):And the coqlib will disappear as well I believe
Matthieu Sozeau (Mar 30 2021 at 17:30):Just -indices-matter
Michael Soegtrop (Mar 30 2021 at 17:30):I see.
Michael Soegtrop (Mar 30 2021 at 17:30):This solves the path issue.
Michael Soegtrop (Mar 30 2021 at 17:30):Will this be merged early enough before the workshop?
Ali Caglayan (Mar 30 2021 at 17:30):I merged my PR upstream, you should be able to use coqide with HoTT np
Michael Soegtrop (Mar 30 2021 at 17:31):Ah, it is already merged? We just need to update the opam package?
Matthieu Sozeau (Mar 30 2021 at 17:31):Cool. Can you make a point release for Coq-8.13?
Ali Caglayan (Mar 30 2021 at 17:31):HoTT passes two important flags to coq -noinit and indices-matter
Michael Soegtrop (Mar 30 2021 at 17:31):Ah, the -noinit replaces the -coqlib?
Ali Caglayan (Mar 30 2021 at 17:32):yep
Michael Soegtrop (Mar 30 2021 at 17:32):nice.
Michael Soegtrop (Mar 30 2021 at 17:33):So we recommend HoTT users to use a _CoqProject file with
-arg -noinit
-arg -indices-matter
and remove all teh hoq files?
Ali Caglayan (Mar 30 2021 at 17:33):I'll make an opam release for 13.1
Théo Zimmermann (Mar 30 2021 at 17:33):Michael Soegtrop said:
So we recommend HoTT users to use a _CoqProject file with
-arg -noinit -arg -indices-matterand remove all teh hoq files?
Exactly.
Michael Soegtrop (Mar 30 2021 at 17:33):We can take a local opam patch file in the platform
Michael Soegtrop (Mar 30 2021 at 17:34):(for the time beeing)
Michael Soegtrop (Mar 30 2021 at 17:34):But I have write rights to the Coq opam arhcive, so I could also merge a PR.
Matthieu Sozeau (Mar 30 2021 at 17:35):It'll be cleaner with a release, which we can put in the released repo of Coq instead of extra-dev and use it for the Coq Platform release
Michael Soegtrop (Mar 30 2021 at 17:35):This all looks like a much nicer solution now. Having a _CoqProject file with simple options shouldn't kill anybody.
Michael Soegtrop (Mar 30 2021 at 17:36):Yes, but as I said, for testing it might be better to have a local patch in Coq platform first.
Michael Soegtrop (Mar 30 2021 at 17:36):I tend to do it that way for new stuff.
Michael Soegtrop (Mar 30 2021 at 17:36):If it all works as expected, we can still push it to the opam repo.
Matthieu Sozeau (Mar 30 2021 at 17:37):As you prefer then
Michael Soegtrop (Mar 30 2021 at 17:37):I think it is the better approach. In Coq release we should only push stuff which is somehow tested.
Michael Soegtrop (Mar 30 2021 at 17:38):@Matthieu Sozeau : do you take care of it? I can then later test the result on Windows as soon as CI is through. But I could also do it.
Matthieu Sozeau (Mar 30 2021 at 17:39):If you have time now, go ahead, otherwise I'll work on it tomorrow morning
Michael Soegtrop (Mar 30 2021 at 17:39):OK, then I will do it now.
Matthieu Sozeau (Mar 30 2021 at 17:39):Cool, thanks everyone!
Michael Soegtrop (Mar 30 2021 at 17:40):@Ali Caglayan : can you give me the commit hash ot tag I shall use in the opam file?
Ali Caglayan (Mar 30 2021 at 17:41):67cdb33f91a1fba2f4d8413757ab9813c2652bf4
Ali Caglayan (Mar 30 2021 at 17:41):but I am working on a release with a tag and an opam release
Michael Soegtrop (Mar 30 2021 at 17:41):@Ali Caglayan : are the build instruction in this opam file still OK:
https://github.com/coq/platform/blob/007c0075fd4c62f69d6fb3a6b0056143e2e00186/opam/packages/coq-hott/coq-hott.8.13/opam
As I said, let's first test it with a local opam patch (the Coq platform has a local opam patch repo which makes this easy).
Ali Caglayan (Mar 30 2021 at 17:42):So with my latest PR which got merged, you can use coq_makefile to build the library
Ali Caglayan (Mar 30 2021 at 17:42):at least just the vo files
Michael Soegtrop (Mar 30 2021 at 17:43):I would prefer to wait with the release until we tested it in the platform
Ali Caglayan (Mar 30 2021 at 17:43):if you want to build documentation etc you still have to use the old makefile
Michael Soegtrop (Mar 30 2021 at 17:43):Can you send me the build and install instructions you would recommend?
Ali Caglayan (Mar 30 2021 at 17:44):After cloning the repo, inside the HoTT directory run:
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile
this ofcourse requires coq_makefile to be around
Michael Soegtrop (Mar 30 2021 at 17:45):coq_makefile is part of teh coq opam package
Ali Caglayan (Mar 30 2021 at 17:45):so it should be fine?
Ali Caglayan (Mar 30 2021 at 17:46):I think I will do the opam release with this build method btw
Ali Caglayan (Mar 30 2021 at 17:46):but the "official" build instructions on the repo still suggest using the old makefile
Ali Caglayan (Mar 30 2021 at 17:46):I just haven't had the time to update this yet
Michael Soegtrop (Mar 30 2021 at 17:46):As I said, let's test it and see ...
Michael Soegtrop (Mar 30 2021 at 18:00):OK, a local Windows build is running ...
Ali Caglayan (Mar 30 2021 at 18:16):OK i've submitted an opam archive PR that uses the new way of building the library https://github.com/coq/opam-coq-archive/pull/1668
Ali Caglayan (Mar 30 2021 at 18:50):@Michael Soegtrop my opam build seems to be successful. How is your testing going?
Michael Soegtrop (Mar 30 2021 at 18:50):M ylocal build works as expected with a _CoqProject file.
Michael Soegtrop (Mar 30 2021 at 18:50):I push to @Matthieu Sozeau PR branch to run CI.
Michael Soegtrop (Mar 30 2021 at 18:51):We can compare our opam files then.
Ali Caglayan (Mar 30 2021 at 18:52):opam-version: "2.0"
maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
homepage: "http://homotopytypetheory.org/"
bug-reports: "https://github.com/HoTT/HoTT/issues"
license: "BSD-2-Clause"
build: [
["coq_makefile" "-f" "_CoqProject" "-o" "CoqMakefile"]
[make "-f" "CoqMakefile" "-j%{jobs}%"]
]
install: [make "-f" "CoqMakefile" "install"]
depends: [
"ocaml"
"ocamlfind" {build}
"coq" {>= "8.13" & < "8.14~"}
]
authors: ["The Coq-HoTT Development Team"]
dev-repo: "git+https://github.com/HoTT/HoTT.git"
synopsis: "The Homotopy Type Theory library"
tags: [ "logpath:HoTT" ]
url {
src: "git+https://github.com/HoTT/HoTT.git#V8.13.1"
}
I made a V8.13.1 tag for the HoTT library btw
Michael Soegtrop (Mar 30 2021 at 18:53):For performance reasons it is prefered to use tar.gz files for releases.
Michael Soegtrop (Mar 30 2021 at 18:53):opam-version: "2.0"
maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
homepage: "http://homotopytypetheory.org/"
bug-reports: "https://github.com/HoTT/HoTT/issues"
license: "BSD-2-Clause"
build: [
["coq_makefile" "-f" "_CoqProject" "-o" "CoqMakefile"]
[make "-j%{jobs}%" "-f" "CoqMakefile"]
]
install: [make "-f" "CoqMakefile" "install"]
depends: [
"ocaml"
"ocamlfind" {build}
"coq" {>= "8.13" & < "8.14~"}
]
authors: ["The Coq-HoTT Development Team"]
dev-repo: "git+https://github.com/HoTT/HoTT.git"
synopsis: "The Homotopy Type Theory library"
tags: [ "logpath:HoTT" ]
url {
src: "https://github.com/HoTT/HoTT/archive/67cdb33f91a1fba2f4d8413757ab9813c2652bf4.tar.gz"
checksum: "sha512=421fddf05417c92aa0c35532efd5da4258bef0f0f6221ffcd3507b30a88b180cccb1bd25d6e5eb0349d4da007bf46a0a1f2b0dab09ac8386ea28f7c471496622"
}
Ah I wasn't aware of this
Michael Soegtrop (Mar 30 2021 at 18:57):CI is running here: (https://github.com/coq/platform/pull/97)
As I said, local tests on Windows did work with this _CoqProject file:
-arg -noinit
-arg -indices-matter
Opening a .v file using HoTT from the same folder as this _CoqProject file works with plain coqide.
Michael Soegtrop (Mar 30 2021 at 18:58):So all in all it is pretty nice now!
Michael Soegtrop (Mar 30 2021 at 18:58):I guess you know how to compute the SHA code ...
Ali Caglayan (Mar 30 2021 at 18:59):No not really. How do you do it?
Michael Soegtrop (Mar 30 2021 at 19:01): Ali Caglayan (Mar 30 2021 at 19:02):Stupid question: What's the point of a checksum here?
Michael Soegtrop (Mar 30 2021 at 19:04):It makes sure nobody can tamper with the source code. You must have exactly the source code specified in the opam file with this hash.
Michael Soegtrop (Mar 30 2021 at 19:04):For git this is not required because it is considered to be reasonably safe on its own.
Michael Soegtrop (Mar 30 2021 at 19:05):I am gone for today! LetÄs continue tomorrow. What timezone are you in?
Ali Caglayan (Mar 30 2021 at 20:18):@Michael Soegtrop I'm in Europe time
Michael Soegtrop (Mar 31 2021 at 06:49):@Matthieu Sozeau : on Windows the opam package of @Ali Caglayan works. I guess on other platforms we have to remove the HoTT specific hacks, e.g. the config file does not exist any more. I wonder if it wouldn't be easier to start from scratch from @Enrico Tassi's DMG PR. What is your opinion on this?
@Enrico Tassi : I have time to finalize the DMG stuff over easter. So how about making a normal release after easter including HoTT? @Matthieu Sozeau : would this fit your time line?
Michael Soegtrop (Mar 31 2021 at 07:02):Btw.: is it possible to sneak into some introductory lectures on HoTT?
Bas Spitters (Mar 31 2021 at 07:12):@Michael Soegtrop Of course! Just sign up for the school, and we promise not to fail you for not attending all the lectures. :-)
Many thanks for your help on the HoTT platform.
Ali Caglayan (Mar 31 2021 at 07:37):@Michael Soegtrop Hopefully the opam package looks better now. I couldn't find any documentation, but what am I allowed to put inside the description string? I've used markdown syntax hopefully it is ok.
Matthieu Sozeau (Mar 31 2021 at 07:37):Hello! Great news! I can just rebase interactively and remove the unneeded stuff
Matthieu Sozeau (Mar 31 2021 at 07:38):@Ali Caglayan you mean the opam package?
Ali Caglayan (Mar 31 2021 at 07:38):Yes, sorry, still waking up :-)
Matthieu Sozeau (Mar 31 2021 at 07:49):I think we should give a logical name to contrib/, e.g. HoTT.contrib
Ali Caglayan (Mar 31 2021 at 07:50):I think part of the reason a logical name hadn't been given was that it wasn't really supposed to be used.
Enrico Tassi (Mar 31 2021 at 07:56):I'm fine with a 2021.02.2 = 2021.02.1 + DMG + coq-hott if that helps a school.
Glad to see that hott is finally just a library and a few flags
Matthieu Sozeau (Mar 31 2021 at 08:03):The thing is it gets installed in user-contrib/'', which is clearly wrong
Matthieu Sozeau (Mar 31 2021 at 08:04):@Enrico Tassi @Michael Soegtrop If you can make it happen that'd be great :)
Ali Caglayan (Mar 31 2021 at 08:16):I think we should then update the install step not to install things from contrib
Ali Caglayan (Mar 31 2021 at 08:17):currently it is the default makefile install
Ali Caglayan (Mar 31 2021 at 08:17):But I don't know how to blacklist things from being installed there
Matthieu Sozeau (Mar 31 2021 at 08:24):Not sure coq_makefile has that ability. We can have an additional _ContribProject file though, that would be the cleanest
Michael Soegtrop (Mar 31 2021 at 08:48):Ali Caglayan said:
Michael Soegtrop Hopefully the opam package looks better now. I couldn't find any documentation, but what am I allowed to put inside the description string? I've used markdown syntax hopefully it is ok.
The description is plain text (unicode). It observes new lines. E.g. coq-elpi always had an elaborate description. You can use opam show coq-hott to look at the description.
Michael Soegtrop (Mar 31 2021 at 08:51):@Matthieu Sozeau : what exactly is the problem? On Windows it got installed under user-contrib/HoTT, which is where it should go now since it just needs a few extra options in a _CoqProject file to work.
Matthieu Sozeau (Mar 31 2021 at 08:54):Most of the files get installed right, but the two in contrib/ are problematic
Matthieu Sozeau (Mar 31 2021 at 08:54):Locally, I see them get installed in lib/coq/user-contrib/''
Michael Soegtrop (Mar 31 2021 at 08:57):I see, I can check later in Windows around noon.
Matthieu Sozeau (Mar 31 2021 at 09:01):I rebased the PR removing the macos specific patching. It might be worth keeping the packages built by the PR as they are much smaller than a full platform I think.
Michael Soegtrop (Mar 31 2021 at 09:04):@Matthieu Sozeau : the Coq Platform explicitly encourages it to create strip down and/or extended variants e.g. for courses, but we wouldn't offer these on the official release page.
Matthieu Sozeau (Mar 31 2021 at 09:05):Ok, that's fine. I'm sure I can find somewhere to host them.
Ali Caglayan (Mar 31 2021 at 09:09):@Michael Soegtrop We already have tags: [ "logpath:HoTT" ] btw
Michael Soegtrop (Mar 31 2021 at 09:09):Regarding the install issues: it is common to have a wrapper makefile around coq_makefile which does a few extra things.
Ali Caglayan (Mar 31 2021 at 09:10):Yeah, this isn't our main setup yet
Ali Caglayan (Mar 31 2021 at 09:10):I am working on untangling our current makefile
Ali Caglayan (Mar 31 2021 at 09:10):Eventually that will call the one generated by coq_makefile
Michael Soegtrop (Mar 31 2021 at 09:12):@Ali Caglayan : ah, yes modal blindness, the tag is there. So just please adjust the description and squash your commits, then I will merge.
Ali Caglayan (Mar 31 2021 at 09:16):OK I have squashed the commits
Michael Soegtrop (Mar 31 2021 at 09:24):@Ali Caglayan : thanks - after Matthieu's remark I need to do some additional checks about files installed directly in user-contrib. I will do so after lunch.
Michael Soegtrop (Mar 31 2021 at 14:59):@Ali Caglayan : I did some tests. The issue with installing under user-contrib/'' can be solved by setting:
-R theories HoTT
-Q contrib HoTT.contrib
One can of course use any other path like e.g. HoTT.book.
Btw.: The HoTTbook files need to be adjusted to Require HoTT.HoTT, otherwise they won't run.
I would put a suitable _CoqProject file into the HoTT book folder, so that people can open the files from there from CoqIDE without issues. One can handle this as an extra install command in the opam file.
Michael Soegtrop (Mar 31 2021 at 15:00):And is discussed in the PR, I was assuming that this is a release PR - that's the reason I was so picky. It has to be a release PR if you want to use it in Coq Platform without copying it there.
Michael Soegtrop (Mar 31 2021 at 15:01):If you want to keep it in extra-dev, it should be named .beta and not .dev, since it is not a classical dev package (which would target master and not a specific commit or tag).
Emilio Jesús Gallego Arias (Mar 31 2021 at 15:40):@Ali Caglayan I see you are not passing -boot to Coq, do you want to keep the Coq.* prefix in scope?
Emilio Jesús Gallego Arias (Mar 31 2021 at 15:41):I recommend you don't keep it unless needed, this way you can just have coq-hott depend on coq-core
Ali Caglayan (Mar 31 2021 at 17:16):Yeah, so passing -boot makes things much more complicated here
Ali Caglayan (Mar 31 2021 at 17:17):I need to then explicitly find the ltac and numeral notations plugin
Ali Caglayan (Mar 31 2021 at 17:17):or at least get _CoqProject to point to them
Ali Caglayan (Mar 31 2021 at 17:17):in my testing, everything was working fine without the flag
Emilio Jesús Gallego Arias (Mar 31 2021 at 17:18):I see, you want to keep only the -I part
Emilio Jesús Gallego Arias (Mar 31 2021 at 17:18):makes sense, tho note that if we manage to for 8.14 you can hopefully still depend only on coq-core and avoid locating the plugins
Michael Soegtrop (Mar 31 2021 at 17:20):@Ali Caglayan : are you doing the changes I suggested to get rid of the files under user-contrib/'' ?
Emilio Jesús Gallego Arias (Mar 31 2021 at 17:20):(deleted)
Emilio Jesús Gallego Arias (Mar 31 2021 at 17:20):as when https://github.com/coq/coq/pull/14019 is merged you can just do Require ML Module "coq.plugins.ltac" and Coq will find the plugin for you.
Ali Caglayan (Mar 31 2021 at 17:20):@Michael Soegtrop Yes, I'm taking a look now
Ali Caglayan (Mar 31 2021 at 17:22):I'm not super sure what to do about the fact that this is a dev package however
Michael Soegtrop (Mar 31 2021 at 17:27):Just move it to released and remove the .dev extension.
Michael Soegtrop (Mar 31 2021 at 17:28):We can test it in Coq platform before we inally commit it, but if it is used during the Spring School, there is no good reason for not making it a release package (except that it should point to a HoTT tag then).
Michael Soegtrop (Mar 31 2021 at 17:29):I undertsood you such that you plan to do a HoTT release based on the commit after testing it.
Ali Caglayan (Mar 31 2021 at 17:30):Yeah, I can do a release for that
Ali Caglayan (Mar 31 2021 at 17:30):let me get the changes to _CoqProject sorted first
Michael Soegtrop (Mar 31 2021 at 17:30):But lets' wait until everything is nice and clean in Coq platform.
Michael Soegtrop (Mar 31 2021 at 17:31):OK fine. I would think that this is the most user friendly HoTT version so far, so it makes sense to officially release it.
Ali Caglayan (Mar 31 2021 at 17:39):OK just checking nothing is breaking: https://github.com/HoTT/HoTT/pull/1433
Ali Caglayan (Mar 31 2021 at 17:42):my local tests seem to indicate it is working as expected
Ali Caglayan (Mar 31 2021 at 17:43):once the ci for HoTT is green I will merge and then we can experiment with an opam release
Michael Soegtrop (Mar 31 2021 at 17:45):@Ali Caglayan : you might want to choose a folder name like HoTT_book, so that people find it. Also please remember to edit the files such that they actually work with a HoTT in user-contrib and provide a _CoqProject file one can copy during opam install.
Michael Soegtrop (Mar 31 2021 at 17:45):Contrib sounds more like "stuff you might want to look at much later".
Ali Caglayan (Mar 31 2021 at 17:46):Ah but I was weary of including contrib to begin with. In general, I don't think anybody in the HoTT library wants users to use those files.
Matthieu Sozeau (Mar 31 2021 at 17:50):Then I suggest we use a separete _ContribProject file and forget about it when we install
Ali Caglayan (Mar 31 2021 at 17:51):How does that work?
Ali Caglayan (Mar 31 2021 at 17:52):You can think of the files in Contrib as almost being documentation
Ali Caglayan (Mar 31 2021 at 17:56):anyhow, I think keeping the files in HoTT.Contrib is fine for now
Ali Caglayan (Mar 31 2021 at 17:56):doing what mattieu suggests will complicate things on our end for now
Michael Soegtrop (Mar 31 2021 at 17:58):Ah OK, I thought this was a nice tutorial on HoTT users would like to find.
Ali Caglayan (Mar 31 2021 at 17:59):Yeah its just a pointer to places in the library which correspond to definitions/results from the HoTT book.
Michael Soegtrop (Mar 31 2021 at 17:59):@Ali Caglayan : if you don't want to install Contrib in opam, you have the following options:
coq_makefile -f _CoqProjectContrib -o CoqMakefileContrib and mane accordingly. Ali Caglayan (Mar 31 2021 at 18:00):Yeah they both seem fiddly for now, I will keep them installed as they do no harm
Michael Soegtrop (Mar 31 2021 at 18:00):OK. If users are not supposed to find them easily, HoTT.Contrib is just fine.
Michael Soegtrop (Mar 31 2021 at 18:01):Then of cause there is also no need to make them run from CoqIDE.
Michael Soegtrop (Mar 31 2021 at 18:01):(easily)
Ali Caglayan (Mar 31 2021 at 18:01):speaking of CoqIDE, did you test HoTT with it?
Ali Caglayan (Mar 31 2021 at 18:01):I got it working yesterday, but today I am having trouble
Michael Soegtrop (Mar 31 2021 at 18:02):Yes, sure. Works fine as long as you have a _CoqProject file with the two options.
Ali Caglayan (Mar 31 2021 at 18:02):Just tested it now, it's working again
Ali Caglayan (Mar 31 2021 at 18:02):earlier it was getting confused with Coq.Init.Prelude
Michael Soegtrop (Mar 31 2021 at 18:02):Note that when you create a new file within CoqIDE, it won't pick up the _CoqPlatform file. You have to close it and open it again.
Michael Soegtrop (Mar 31 2021 at 18:03):It reads the _CoqProject file only on file open.
Ali Caglayan (Mar 31 2021 at 18:03):yes, I suspected as much
Michael Soegtrop (Mar 31 2021 at 18:03):Also stuff in scratch buffers won't work.
Ali Caglayan (Mar 31 2021 at 18:04):scratch buffers seem to work for me
Ali Caglayan (Mar 31 2021 at 18:04):but I am running from the _CoqProject directory so maybe thats why
Michael Soegtrop (Mar 31 2021 at 18:04):Possibly.
Michael Soegtrop (Mar 31 2021 at 18:05):One just should tell users that the pick up of the _CoqPlatform file does not work in some cases, and then a close + open fixes it.
Ali Caglayan (Mar 31 2021 at 18:36):@Michael Soegtrop Alright how is this: https://github.com/coq/opam-coq-archive/pull/1671
Ali Caglayan (Mar 31 2021 at 18:36):I haven't created a tag yet in the HoTT library so we can definitely be sure it works
Michael Soegtrop (Apr 01 2021 at 06:41):Thanks, I will test it today and tomorrow. Are you available over the easter days? I plan to finalize the DMG package, so that we can do a new Platform release early next week.
@Enrico Tassi : you said that there will be a new Coq patch release. Do you have a schedule for it?
Enrico Tassi (Apr 01 2021 at 07:02):The pr is merged https://github.com/coq/coq/pull/14005 I will backport it today and see if I can tag.
Enrico Tassi (Apr 01 2021 at 07:04):Next week I will be busy, but If you do the release I can find a minute to upload the snap an sign windows pkg
Michael Soegtrop (Apr 01 2021 at 07:53):@Enrico Tassi : sounds good, so let#s plan for that.
Ali Caglayan (Apr 01 2021 at 15:13):@Michael Soegtrop I should be available over Easter
Michael Soegtrop (Apr 01 2021 at 17:22):@Ali Caglayan : good - I will ping you here every now and again ...
Michael Soegtrop (Apr 06 2021 at 19:21):@Ali Caglayan : sorry, the Mac stuff took a bit longer. I am currently testing your package. It points to master, rather than a specific commit. Which commit should I test (the one you want to tag)?
Michael Soegtrop (Apr 06 2021 at 19:26):I would also need one file from the repo to test for the smoke test kit. The file should run through in no more than 10 seconds and do some not entirely trivial HoTT.
Ali Caglayan (Apr 06 2021 at 21:13):dd3c399d6c6c9275c3f4b9feee46925f8f415f49
Ali Caglayan (Apr 06 2021 at 21:14):https://github.com/HoTT/HoTT/blob/master/theories/Homotopy/BlakersMassey.v
Matthieu Sozeau (Apr 06 2021 at 21:56):@Michael do you already have a coq-platform release I could point to? We're opening the school tomorrow, letting the students prepare and it could be nice to have it, although I already have functional releases with just HoTT.
Michael Soegtrop (Apr 07 2021 at 06:38):@Matthieu Sozeau : not yet, but likely around noon - the installers will be unsigned, though.
Michael Soegtrop (Apr 07 2021 at 06:52):@Matthieu Sozeau @Ali Caglayan : one note: as a test I did put a _CoqProject file with the proper options into the Coq Platform install folder of HoTT. This allows people to open and run HoTT files from the install folder in CoqIDE - which can be a great help to understand things. But this does not work for all files, because some files reference HoTT files without the HoTT prefix. It would help users to change all files such that this does work. As examples:
Homotopy/Join.vExcludedMiddle.vRequire Import Hott.XYZ. Michael Soegtrop (Apr 07 2021 at 07:04):Btw.: the recommended test file doesn't work either for this reason: it has: `Require Import HoTT.Basics HoTT.Types HProp.. The first required module name is fine, the second not. I will choose another file to make CI happy.
Michael Soegtrop (Apr 07 2021 at 07:07):I picked theories/Analysis/Locator.v.
Matthieu Sozeau (Apr 07 2021 at 07:59):I think that's fair to ask for cleanly qualified names in a library.
Michael Soegtrop (Apr 07 2021 at 08:19):Maybe the From HoTT Require ... syntax helps to keep the require statements readable.
Ali Caglayan (Apr 07 2021 at 08:20):Ah ok, so this causes problems outside of the library
Ali Caglayan (Apr 07 2021 at 08:20):Jason has a script that can qualify modules IIRC
Michael Soegtrop (Apr 07 2021 at 08:23):@Ali Caglayan : it won't cause problems for people using HoTT as a library. But it causes problems for people who want to load a file from the HoTT library and single step through it to understand the proofs without locally recompiling HoTT. I would expect that for HoTT this is something people might want to do.
If one adds a _CoqProject file to the root of the HoTT install folder and fixes the Require statement a user could load any file from the HoTT installation or from downloaded compatible HoTT sources and just step through them. I find it rather annoying if I have to recompile a library to do that. And even then it is not always easy, because one has to figure out the correct -Q and -R options for CoqIDE.
Michael Soegtrop (Apr 07 2021 at 08:26):So under the line this improves the situation for HoTT learners considerably.
Ali Caglayan (Apr 07 2021 at 08:28):The problem is that some of our developers like to write short and snappy requires. I agree that it is better to fully qualify names but I also sympathise with people who do not like to do this.
Ali Caglayan (Apr 07 2021 at 08:28):Last year we discussed changing the requires to their full length, but I don't think we reached a consensus.
Ali Caglayan (Apr 07 2021 at 08:29):Is Coq really not able to elaborate the module names? It looks to me like a useful feature.
Michael Soegtrop (Apr 07 2021 at 08:30):Actually From ... Require has -R semantics.
Michael Soegtrop (Apr 07 2021 at 08:30):So all you need to do for having things work technically is to prepend all Require statements which are not qualified with From HoTT.
Ali Caglayan (Apr 07 2021 at 08:31):I suppose this works, but from the point of view of writing the library it seems a bit silly to write From HoTT everywhere in it?
Ali Caglayan (Apr 07 2021 at 08:32):But I can give it a go in a branch and see how it works if you like
Michael Soegtrop (Apr 07 2021 at 08:32):Well it is a question of coexistance. E.g. some files have a Require Basics. But there is a Basics.v in the standard library and you will get this then.
Michael Soegtrop (Apr 07 2021 at 08:33):Actually I think this is something you want to fix for the school. It really makes the live of people who want to learn this unnecessarily hard.
Théo Zimmermann (Apr 07 2021 at 08:37):Ali Caglayan said:
I suppose this works, but from the point of view of writing the library it seems a bit silly to write
From HoTTeverywhere in it?
Agreed. I think it was indeed discussed recently that the semantics should be that From X is implicit whenever you are working on X.
Ali Caglayan (Apr 07 2021 at 08:40):Eugh, some of our files already have the HoTT qualification which makes my life harder
Michael Soegtrop (Apr 07 2021 at 08:40):@Théo Zimmermann : but how would you do this technically? Say someone is downloading the HoTT sources, opens a file in CoqIDE and wants to step through them? How is Coq supposed to know that you are in HoTT? Maybe a _CoqProject file would help if -Q and -R would support relative paths. Another option would be to have a statement just From HoTT. or whatever Syntax, which sets a default From.
Michael Soegtrop (Apr 07 2021 at 08:41):@Ali Caglayan : I have an awk book, so it probably doesn't take me longer than 10 minutes. Shall I do it?
Théo Zimmermann (Apr 07 2021 at 08:41):Yes, basically the _CoqProject file -R / -Q option would do the job (they do support relative paths of course, what do you mean by your point about this?)
Ali Caglayan (Apr 07 2021 at 08:41):I'll try one more thing first
Michael Soegtrop (Apr 07 2021 at 08:42):@Théo Zimmermann : I mean they would have to support relative paths with respect to coqc -where and not relative to pwd.
Michael Soegtrop (Apr 07 2021 at 08:43):Some time back I suggested to add a -V option which would be like -Q but relative to coqc -where.
Ali Caglayan (Apr 07 2021 at 08:45):Well coq is complaining here: We have a line like Require HoTT.Tactics in a file, so I went and removed the HoTT. to get Require Tactics and then replaced Require with From HoTT Require, but now coq complains about From HoTT Require Tactics since Tactics is ambiguous
Michael Soegtrop (Apr 07 2021 at 08:46):@Ali Caglayan in such cases you either use Require without From or you give a longer Path with From, which makes the files unique.
Théo Zimmermann (Apr 07 2021 at 08:47):If the fullname is HoTT.Tactics, I don't think you have any solution with From.
Ali Caglayan (Apr 07 2021 at 08:47):@Michael Soegtrop I can't make that one longer though, since From HoTT Require HoTT.Tactics won't work
Michael Soegtrop (Apr 07 2021 at 08:47):Let me check. Which file are you at?
Ali Caglayan (Apr 07 2021 at 08:48):Categories/GroupoidCategory/Morphisms.v for example
Ali Caglayan (Apr 07 2021 at 08:48):Ok so if I decide to leave the HoTT. in I run into more trouble, because some Require statements are doing multiple: Require HoTT.Basics Foo.bar
Ali Caglayan (Apr 07 2021 at 08:48):So now I would have to split those up...
Michael Soegtrop (Apr 07 2021 at 08:49):Yes, mixed requires need to be split - at which point AWK or whatever tools Jason has might become useful.
Ali Caglayan (Apr 07 2021 at 08:50):This is what I did for reference:
ali:~/HoTT$ find theories/ -type f -name "*.v" -exec sed -i 's/HoTT.//g' {} \;
ali:~/HoTT$ find theories/ -type f -name "*.v" -exec sed -i 's/Require /From HoTT Require /g' {} \;
Not sure if this is going to work ...
Ali Caglayan (Apr 07 2021 at 08:51):Yeah it doesn't :sweat_smile:
Michael Soegtrop (Apr 07 2021 at 08:55):It is indeed nasty because you have so many duplicate names
Michael Soegtrop (Apr 07 2021 at 08:56):I guess one needs to look into the .d files to get this sorted out.
Michael Soegtrop (Apr 07 2021 at 08:57):For example you have this:
./Categories/Category/Sigma/Core.v
./Categories/Category/Core.v
There is no way to require the second file with From Require without a warning.
Théo Zimmermann (Apr 07 2021 at 08:58):Wouldn't From HoTT Require Category.Core work in this case?
Michael Soegtrop (Apr 07 2021 at 08:58):Ah yes ...
Michael Soegtrop (Apr 07 2021 at 09:00):@Ali Caglayan : so for the file you mentioned, this does work:
From HoTT.Basics Require Trunc Equivalences.
From HoTT.Categories Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core Tactics.
Yeah typically with names like Core they will be qualified as they appear in a lot of places in the library.
Michael Soegtrop (Apr 07 2021 at 09:01):Originally it was
Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core.
Require Import Trunc Equivalences HoTT.Tactics.
But I messed it up, you have to use:
From HoTT.Basics Require Trunc Equivalences.
From HoTT.Categories Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core.
Require HoTT.Tactics.
I got the wrong Tactics file above.
Michael Soegtrop (Apr 07 2021 at 09:03):So as I said, since it is that complicated I would look at the .d files and create the Require statements from that.
Ali Caglayan (Apr 07 2021 at 09:07):I like the idea of having a From HoTT. statement that sets the default form.
Ali Caglayan (Apr 07 2021 at 09:09):Maybe it could even be inherited on import, that way we only need one From HoTT in the whole library
Michael Soegtrop (Apr 07 2021 at 09:09):But I guess it wouldn't work for the level of complexity you have in HoTT.
Michael Soegtrop (Apr 07 2021 at 09:22):So how shall we proceed? Do you have the scripts from Jason you mentioned?
Ali Caglayan (Apr 07 2021 at 09:28):I think I am misremembering then
Ali Caglayan (Apr 07 2021 at 09:29):I can't find Jason's scripts
Ali Caglayan (Apr 07 2021 at 09:29):I can only find one which minimizes requires and imports
Ali Caglayan (Apr 07 2021 at 09:31):Oh no it exists
Ali Caglayan (Apr 07 2021 at 09:32):https://coq.inria.fr/related-tools.html
Ali Caglayan (Apr 07 2021 at 09:32):at the bottom
Ali Caglayan (Apr 07 2021 at 09:32):https://github.com/JasonGross/coq-tools/blob/master/move-requires.py
Ali Caglayan (Apr 07 2021 at 09:33):There are quite a few scripts there that might be useful
Michael Soegtrop (Apr 07 2021 at 09:33):Looks too simple to be likely to work.
Michael Soegtrop (Apr 07 2021 at 09:34):I guess there is no way one can get the Require statements right without looking into the .v.d files. One needs some artifacts which have info from what the -Q and -R options where during compile.
Matthieu Sozeau (Apr 07 2021 at 09:51):Yup. I dream of a day where we can program such things in MetaCoq :)
Matthieu Sozeau (Apr 07 2021 at 09:51):Just load the .vos, crawl the environment and output the minimal dependencies for each file
Matthieu Sozeau (Apr 07 2021 at 09:52):Even coqdep is not good enough because it relies on the Imports in the file, some of which might be unnecessary
Gaëtan Gilbert (Apr 07 2021 at 09:54):You can't tell which imports are necessary, there can be arbitrary notations, hints, etc in there
Michael Soegtrop (Apr 07 2021 at 09:57):Well I would take the Require statements from the files and just figure out the proper qualification from the .v.d files.
Ali Caglayan (Apr 07 2021 at 10:08):I'm not having much success with Jason's scripts
Matthieu Sozeau (Apr 07 2021 at 10:09):Of course that would require knowing something about the libobjects too, hence we couldn't do it today
Michael Soegtrop (Apr 07 2021 at 10:47):@Ali Caglayan : I expected that. If you want I can have a look at it.
Ali Caglayan (Apr 07 2021 at 10:48):That would be great
Michael Soegtrop (Apr 07 2021 at 10:48):OK, after lunch ...
Michael Soegtrop (Apr 07 2021 at 10:50):Btw.: The Coq Platform Test CI ran though - including smoke tests on Windows and Mac: (https://github.com/coq/platform/pull/99). You can download full Mac, Windows and Linux installers from the CI artifacts.
Michael Soegtrop (Apr 07 2021 at 10:50):(I used a local HoTT opam file in the patch repo).
Matthieu Sozeau (Apr 07 2021 at 12:04):Great news!
Michael Soegtrop (Apr 07 2021 at 16:16):@Ali Caglayan : sorry I was busy with other things ...
I had a look at Jason's tools and I think you just picked the wrong one.
This does work (in the HoTT folder - adjust the path to the python script):
python2 ../coq-tools/absolutize-imports.py --update-all -f _CoqProject
It doesn't introduce From prefixes but makes all paths absolute with HoTT prefix. IMHO that doesn't look that bad and might even be more informative to non expert users. I would suggest you take a look yourself.
Automatically introducing Form statements is more tricky than making paths absolute, because one need to consider if a path is unique or not with a From. After looking at it in more detail, I would actually advise against using From for HoTT - it might be error prone cause of the duplicate names.
Michael Soegtrop (Apr 07 2021 at 16:17):Example before:
Require Import HoTT.Basics HoTT.Types HProp.
Require Import Extensions HoTT.Truncations.
Require Import Modality Accessible Lex Nullification.
and after
Require Import HoTT.Basics HoTT.Types HoTT.HProp.
Require Import HoTT.Extensions HoTT.Truncations.
Require Import HoTT.Modalities.Modality HoTT.Modalities.Accessible HoTT.Modalities.Lex HoTT.Modalities.Nullification.
I think it might be a feasible workflow for you to let developers write what they want and then run Jason's tool over it before each release to normalize it.
Michael Soegtrop (Apr 07 2021 at 16:18):As I said, I do find it more readable that way, and I think code should be optimized for readability.
Matthieu Sozeau (Apr 07 2021 at 16:58):FWIW, I can run HoTT on the provided MacOS Installer from the CI just fine
Michael Soegtrop (Apr 07 2021 at 17:00):@Matthieu Sozeau : yes, this is expected. As I said above there is no issue with using HoTT as a library with the Requires as is. What does not work is open a HoTT library file in CoqIDE and step through it. This is something learners might want to do.
Matthieu Sozeau (Apr 07 2021 at 17:00):Indeed, that could happen
Michael Soegtrop (Apr 07 2021 at 17:01):So especially for a HoTT school one might want to change this.
Michael Soegtrop (Apr 07 2021 at 17:01):Applying Jason's script as above fixes this.
Michael Soegtrop (Apr 07 2021 at 17:04):Also for a new comer the short require statements are hard to understand. It does help to be explicit here and tell which module comes from where.
Ali Caglayan (Apr 07 2021 at 17:19):Excellent to hear that you got that script working! I also tried that one but it looks like you are more patient then me :-)
Ali Caglayan (Apr 07 2021 at 17:20):I'll try and do a PR later
Michael Soegtrop (Apr 07 2021 at 17:26):I hope @Matthieu Sozeau agrees to this change. If so please tag it after the change - I can update and merge your opam PR then.
Matthieu Sozeau (Apr 07 2021 at 17:27):I'm fine with it!
Michael Soegtrop (Apr 08 2021 at 06:53):@Ali Caglayan : any progress with this? This should be really quick. I can also make a PR for it.
Ali Caglayan (Apr 08 2021 at 09:17):Sorry I didn't have the time for it, I can quickly do it now
Michael Soegtrop (Apr 08 2021 at 09:30):OK. I can take care of the opam packages as soon as you have a tag.
Ali Caglayan (Apr 08 2021 at 09:35):The script is taking some time to run!
Ali Caglayan (Apr 08 2021 at 10:00):Ah the way you called the script caused Basics to get extended to Coq.Program.Basics
Ali Caglayan (Apr 08 2021 at 10:00):I need to set the coqc and try again
Ali Caglayan (Apr 08 2021 at 10:01):It took roughly half an hour to finish it last time
Ali Caglayan (Apr 08 2021 at 10:18):I also need it to stop crawling in the coq submodule
Ali Caglayan (Apr 08 2021 at 10:18):That seems to have imporved the timing
Ali Caglayan (Apr 08 2021 at 10:44):OK I finally got the script to work. It actually doesn't take long at all, the reason it was taking so long was because it had so many errors to output.
Ali Caglayan (Apr 08 2021 at 10:45):I really didn't think about building the library first...
Ali Caglayan (Apr 08 2021 at 10:45):But now it looks like it has worked I will crate a PR
Gaëtan Gilbert (Apr 08 2021 at 11:00):Why doesn't -R theories HoTT in the coqproject work?
Ali Caglayan (Apr 08 2021 at 11:00):@Gaëtan Gilbert Can I have some more context?
Gaëtan Gilbert (Apr 08 2021 at 11:10):IIUC the goal is that after installing the platform users can open the installed hott .v files and run them interactively
to do that it should suffice to have a _CoqProject file nearby with the right arguments
Ali Caglayan (Apr 08 2021 at 11:12):I didn't test this myself but:
Michael Soegtrop said:
Matthieu Sozeau Ali Caglayan : one note: as a test I did put a _CoqProject file with the proper options into the Coq Platform install folder of HoTT. This allows people to open and run HoTT files from the install folder in CoqIDE - which can be a great help to understand things. But this does not work for all files, because some files reference HoTT files without the HoTT prefix. It would help users to change all files such that this does work. As examples:
- Does not work:
Homotopy/Join.v- Does work:
ExcludedMiddle.v
It is currently not possible to have dynamic absolute paths in _CoqProject files nor is it possible to specify relative paths in -Q and -R options, so there is no easy other fix than changing all files to consistently useRequire Import Hott.XYZ.
Ali Caglayan (Apr 08 2021 at 11:13):So it seems there is a correct _CoqProject but it still doesn't work
Gaëtan Gilbert (Apr 08 2021 at 11:14):doesn't that just mean the _coqproject had incorrect options?
and why would it use absolute paths?
Ali Caglayan (Apr 08 2021 at 11:17):It could be
Mike Shulman (Apr 08 2021 at 11:28):Michael Soegtrop said:
Théo Zimmermann : but how would you do this technically? Say someone is downloading the HoTT sources, opens a file in CoqIDE and wants to step through them? How is Coq supposed to know that you are in HoTT?
Umm, because the file is in the HoTT directory? I must be missing something.
Michael Soegtrop (Apr 08 2021 at 11:52):@Ali Caglayan : I guess you are doing something wrong. For me the scripts takes just a few seconds to run.
Michael Soegtrop (Apr 08 2021 at 11:53):@Gaëtan Gilbert : a _CoqProject files does not work, because it does not support to have relative paths to coqc -where. So one would have to adjust the _CoqProject files to the real absolute paths, which is a bit tricky in installers.
Michael Soegtrop (Apr 08 2021 at 11:54):@Mike Shulman : also a frequent scenario is that people git clone the same or close version as the installed one and step through that.
Michael Soegtrop (Apr 08 2021 at 11:56):@Ali Caglayan : let me just do a PR for that.
Michael Soegtrop (Apr 08 2021 at 12:03):Actually it takes less than 1 second to run ...
Michael Soegtrop (Apr 08 2021 at 12:03):But you need to build before (in the same way as opam does), so that the information is available. Possibly if you do this without building first, the script does something else.
Mike Shulman (Apr 08 2021 at 12:10):Are you saying that if they git clone a different version, then it wouldn't know which version of the files to load with require? But the cloned version will be in its own directory. Coq doesn't ordinarily have trouble looking in the current directory first to find files to load, so why is this any different?
Michael Soegtrop (Apr 08 2021 at 12:11):@Ali Caglayan : https://github.com/HoTT/HoTT/pull/1445
Théo Zimmermann (Apr 08 2021 at 12:12):I think Michael would want to use the compiled version if you clone the repo locally. I'm far from convinced that this is a good idea.
Ali Caglayan (Apr 08 2021 at 12:12):@Michael Soegtrop I already had a PR up: https://github.com/HoTT/HoTT/pull/1444
Michael Soegtrop (Apr 08 2021 at 12:13):@Mike Shulman : you are looking at this from the perspective of a HoTT developer, who has a local nicely compiled build. I talk about students who hardly know how to build the stuff but want to single step through code.
Ali Caglayan (Apr 08 2021 at 12:13):Sorry if I didn't make it clear, I managed to get the script to work
Michael Soegtrop (Apr 08 2021 at 12:14):@Ali Caglayan OK, then please close mine. But honstely I don't know what you are doing here. It really takes just a minute all together including a clean test building after the change.
Ali Caglayan (Apr 08 2021 at 12:14):Yes, I hadn't built the library first
Ali Caglayan (Apr 08 2021 at 12:15):It runs in under a second like you said
Michael Soegtrop (Apr 08 2021 at 12:15):Sorry, I didn't read the last lines of your comment.
Ali Caglayan (Apr 08 2021 at 12:15):I'm actually going to close my PR since something got broken along the way
Michael Soegtrop (Apr 08 2021 at 12:16):OK, I reopen mine then ...
Ali Caglayan (Apr 08 2021 at 12:17):Sorry about athat
Michael Soegtrop (Apr 08 2021 at 12:17):No issue. I will put a few comments into mine how it was done (for reference).
Mike Shulman (Apr 08 2021 at 12:17):Wait a minute, @Michael Soegtrop, are you saying that if there is a local compiled version of HoTT, and someone copies a different version of one file from somewhere, you want them to be able to step through that file and have it load the local compiled version of the files it Requires?
Mike Shulman (Apr 08 2021 at 12:20):That seems to me like a terrible idea; a different version of a file coming from a different version of the library would be likely to also depend on different versions of the other files in the library.
Michael Soegtrop (Apr 08 2021 at 12:20):@Mike Shulman : what I want is that if someone copies any HoTT file from the installed version somewhere where the is no _CoqPlatform file around which tells to do something else, that (s)he can step through it.
Students do want to experiment and this should be made easy without knowing how to clone / compile HoTT.
Say you have HoTT installed via Coq Platform. Now you can just go to GitHub, download a single raw HoTT file and step through it.
Gaëtan Gilbert (Apr 08 2021 at 12:22):use the hoq scripts, otherwise you won't get -indices-matter etc
Michael Soegtrop (Apr 08 2021 at 12:22):If you want a _CoqPlatform file to work it usually means you have to make a local build. I want people to be able to step through the code without making a local build.
Having fully qualified paths doesn't do anything bad to developers.
Michael Soegtrop (Apr 08 2021 at 12:23):@Gaëtan Gilbert : yes you need a _CoqProject file which adds these two arguments for HoTT. The hoqc scripts are gone.
Ali Caglayan (Apr 08 2021 at 12:23):Well not gone as of yet, but not necessary to build the library
Michael Soegtrop (Apr 08 2021 at 12:24):@Ali Caglayan : afaik the opam package does not install them.
Ali Caglayan (Apr 08 2021 at 12:24):Yes, but using the hoq scripts is still the recommended method in the git repo
Ali Caglayan (Apr 08 2021 at 12:24):I just haven't gotten round to doing that change yet
Ali Caglayan (Apr 08 2021 at 12:25):But for someone who is using the library through Platform and doesn't care about compiling HoTT it makes no difference
Michael Soegtrop (Apr 08 2021 at 12:25):OK. I was talking about what is in Opam / the Coq Platform.
Ali Caglayan (Apr 08 2021 at 12:26):Yep, I was just making sure everybody knew what was happening :-)
Michael Soegtrop (Apr 08 2021 at 12:30):So let me summarize, since the discussion took a few turns:
Mike Shulman (Apr 08 2021 at 12:31):Michael Soegtrop said:
what I want is that if someone copies any HoTT file from the installed version somewhere where the is no _CoqPlatform file around which tells to do something else, that (s)he can step through it.
Why? Why can't they just leave it in place and step through it there?
Michael Soegtrop (Apr 08 2021 at 12:31):And yes, one still needs a _CoqProject file, but it contains only the two -arg options.
Michael Soegtrop (Apr 08 2021 at 12:32):Why? Why can't they just leave it in place and step through it there?
As I said, because this only works if you make a local build upfront, which is not easy to do for students.
Théo Zimmermann (Apr 08 2021 at 12:32):Doesn't it work if you run it from the place where it is installed? (If you install both the .vo and the .v)
Théo Zimmermann (Apr 08 2021 at 12:33):Anyway, I think there is something wrong with the assumption that any HoTT library file will be interesting to students.
Théo Zimmermann (Apr 08 2021 at 12:33):IMHO There should be a few well delimited example files with the From HoTT statements so that you can load them with an installed HoTT.
Michael Soegtrop (Apr 08 2021 at 12:34):@Théo Zimmermann : that would be possible if one installs a suitable _CoqProject file. But at least on Mac the files are not easy to find. You need to tell macOS quite explicitly that you want to see the contents of an installed package.
Théo Zimmermann (Apr 08 2021 at 12:35):Right
Michael Soegtrop (Apr 08 2021 at 12:36):Well I can only talk of my experience. I frequently want to step through files to understand them and it is sometimes not easy - even with the above average experience in building stuff I have.
Michael Soegtrop (Apr 08 2021 at 12:36):This is nothing specific to HoTT.
Mike Shulman (Apr 08 2021 at 12:37):So really what we are doing is working around broken behavior of macOS?
Michael Soegtrop (Apr 08 2021 at 12:37):@Mike Shulman : no. The files are not easy to find under .opam in Linux either.
Michael Soegtrop (Apr 08 2021 at 12:38):You won't find them unless you know very well where to look.
Michael Soegtrop (Apr 08 2021 at 12:40):Anyway, why is taken so negatively to just make Require statements more explicit, so that both average humans and machines can digest them better.
Mike Shulman (Apr 08 2021 at 12:40):Huh. It just seems wrong to me to require all the files inside the library to refer to each other with fully-qualified names.
Mike Shulman (Apr 08 2021 at 12:41):It makes the import statements much harder to parse visually for a human, and much more annoying to add new requires when needed.
Michael Soegtrop (Apr 08 2021 at 12:41):Well I would say that with all the duplicate names, it does make it easier.
Mike Shulman (Apr 08 2021 at 12:41):We generally already qualify duplicate names.
Mike Shulman (Apr 08 2021 at 12:41):Sufficiently to disambiguate.
Michael Soegtrop (Apr 08 2021 at 12:41):You can parse something quicker, but you will need much longer to understand what it really means.
Michael Soegtrop (Apr 08 2021 at 12:42):Well I would say it is an issue with the From syntax, that it doesn't work well with the file structure of HoTT.
Michael Soegtrop (Apr 08 2021 at 12:43):It would indeed be nicer to have From HoTT everywhere and then be relaxed, but this doesn't really work for HoTT. Files in the top level folder would still have to be referenced as Require HoTT.XYZ.
Michael Soegtrop (Apr 08 2021 at 12:44):Sufficiently to disambiguate.
If you have been working with HoTT for a few months: yes. For new students: no.
Mike Shulman (Apr 08 2021 at 12:44):Is that just because of duplicate names?
Michael Soegtrop (Apr 08 2021 at 12:45):The problem with From comes from duplicate names, yes.
Mike Shulman (Apr 08 2021 at 12:45):Michael Soegtrop said:
Sufficiently to disambiguate.
If you have been working with HoTT for a few months: yes. For new students: no.
How is it harder than finding a file from a relative path name?
Michael Soegtrop (Apr 08 2021 at 12:45):Things like HoTT.A and HoTT.B.A.
Michael Soegtrop (Apr 08 2021 at 12:47):How is it harder than finding a file from a relative path name?
In HoTT you specify the tail of the qualification, while new comers would be more interested in the head of it.
Mike Shulman (Apr 08 2021 at 12:48):Isn't the "tail" precisely what a relative path name does?
Michael Soegtrop (Apr 08 2021 at 12:48):Isn't the "tail" precisely what a relative path name does?
Well yes. That's the reason why in my PR all paths are absolute below HoTT.
Mike Shulman (Apr 08 2021 at 12:49):If I'm in the directory A/B and I write C/D.v, I know that I mean A/B/C/D.v and not A/E/C/D.v.
Mike Shulman (Apr 08 2021 at 12:49):Even though C/D.v is the "tail" and I've omitted the "head" A/B.
Mike Shulman (Apr 08 2021 at 12:49):Are you saying that your students don't understand relative path names either?
Michael Soegtrop (Apr 08 2021 at 12:49):Well you know this, but an unexpereinces reader which has seen some C/D.f before might assume that it is that same C/D and not a different one.
Michael Soegtrop (Apr 08 2021 at 12:51):To digest that properly, one actually first has to know that there might be two different C/D. Many users won't have this knowledge.
Gaëtan Gilbert (Apr 08 2021 at 12:51):Mike Shulman said:
If I'm in the directory A/B and I write C/D.v, I know that I mean A/B/C/D.v and not A/E/C/D.v.
I don't think that's how Require works
Michael Soegtrop (Apr 08 2021 at 12:52):I don't think that's how Require works
Well that's how it is set up in HoTT with lot's of folder local -Q and -R options.
Mike Shulman (Apr 08 2021 at 12:53):What do other Coq libraries do? Do they fully qualify all imports? Or treat module names as globally unique?
Théo Zimmermann (Apr 08 2021 at 12:54):Other libraries generally do not have duplicated names.
Michael Soegtrop (Apr 08 2021 at 12:54):I would say HoTT as pretty much at the extreme end of having duplicate names.
Gaëtan Gilbert (Apr 08 2021 at 12:54):Michael Soegtrop said:
I don't think that's how Require works
Well that's how it is set up in HoTT with lot's of folder local -Q and -R options.
I only see
-R theories HoTT
-Q contrib HoTT.Contrib
in https://github.com/HoTT/HoTT/blob/master/_CoqProject
Michael Soegtrop (Apr 08 2021 at 12:56):@Gaëtan Gilbert : I think technically it works by having the second last part of the qualification unique (or fairly unique).
Michael Soegtrop (Apr 08 2021 at 12:56):The "folder local -Q -R" is more what is happening in my head when I read HoTT code I guess.
Michael Soegtrop (Apr 08 2021 at 13:01):@Mike Shulman : I think the best way to converge between your and my thinking would be to have a few more options for From. E.g. one could have an option to always choose the shortest path after the From qualification. Then one could always write From HoTT and leave everything else as it is.
Michael Soegtrop (Apr 08 2021 at 13:02):Another option would be to have a From which more works like -Q so that one can put more of the qualification into the From part and group requires this way.
Mike Shulman (Apr 08 2021 at 13:06):To be honest, I'm surprised because I didn't think that we had that many duplicate file names. Doing a quick search and sort, most of the duplicate names I see are in Categories and Classes, both of which were imported into HoTT from previously separate libraries.
Mike Shulman (Apr 08 2021 at 13:07):Anyway, isn't the whole point of namespacing that names don't have to be globally unique?
Michael Soegtrop (Apr 08 2021 at 13:08):Anyway, isn't the whole point of namespacing that names don't have to be globally unique?
Sure, I am a big fan of naming the main type of a module "t".
What I brought up here are purely practical aspects for students.
Michael Soegtrop (Apr 08 2021 at 13:10):I think that distributing HoTT via Opam / Coq Platform brings a few changes in the typical usage patterns of HoTT I think you did not fully adopt to as yet.
Michael Soegtrop (Apr 08 2021 at 13:12):Some people approach projects like HoTT more or less by "playing" with them. All I want is that this isn't made harder than necessary.
Michael Soegtrop (Apr 08 2021 at 13:12):The number of people who approach this by first reading the docs and then following what is written there might be a minority.
Mike Shulman (Apr 08 2021 at 13:16):Gaëtan Gilbert said:
I don't think that's how Require works
Indeed, I see this now looking at the docs:
-R path Libassociates to the file /path/fOO/Bar/File.vo the logical name Lib.fOO.Bar.File, but allows this file to be accessed through the short names fOO.Bar.File,Bar.File and File. If several files with identical base name are present in different subdirectories of a recursive loadpath, which of these files is found first may be system- dependent and explicit qualification is recommended.
It's very counterintuitive to me that name resolution of required files pays no attention to the location of the requiring file in the directory tree, but I guess it's at least consistent with this idea that one ought to be able to pick up a file from anywhere in the library, drop it somewhere else, and still load it.
Mike Shulman (Apr 08 2021 at 13:17):My point is that if the design of the Coq tools essentially forces module names in a library to be globally unique, then something is wrong with that design.
Michael Soegtrop (Apr 08 2021 at 13:18):@Mike Shulman : the names need to be unique inside of the Coq standard library and inside of each development like HoTT but not between developments.
Mike Shulman (Apr 08 2021 at 13:18):I still maintain that something is wrong with that.
Michael Soegtrop (Apr 08 2021 at 13:19):With the standard setup you can't access a HoTT file without HoTT prefix from the outside.
Mike Shulman (Apr 08 2021 at 13:20):Anyway, as regards practical solutions moving forwards, this may be my favorite of the options mentioned, if I understand it correctly:
Another option would be to have a From which more works like -Q so that one can put more of the qualification into the From part and group requires this way.
Michael Soegtrop (Apr 08 2021 at 13:20):Another option would be to have a From which more works like -Q so that one can put more of the qualification into the From part and group requires this way.
Yes, but this would have to be implemented in Coq first, so no option for Coq Platform 2021.02.1.
Mike Shulman (Apr 08 2021 at 13:21):Although always choosing the shortest path after From could work fine too, and might be easier in practice though less informative.
Michael Soegtrop (Apr 08 2021 at 13:26):I agree that the module searching of Coq can be improved in various ways. I guess we should open a CEP - there are a few other issues e.g. handling variants (like CompCert for different CPUs) as well.
Michael Soegtrop (Apr 08 2021 at 13:27):But I would prefer to have this discussion after 2021.02.1 is out - the Coq release manager @Enrico Tassi is waiting for me to tag Coq Platform and I am waiting for HoTT to tag HoTT - either with or without my suggested change.
Michael Soegtrop (Apr 08 2021 at 13:28):If this is highly controversial, we can also have this discussion for the next release and leave things as they are now. All I am saying is that as HoTT is more optimized for HoTT developers than for HoTT users and that this might not be what you want, but in the end this is the decision of the HoTT team.
Matthieu Sozeau (Apr 08 2021 at 13:43):I guess any Require change will have to wait until we have the dune integration and a single code path for handling them in all the tools.
Matthieu Sozeau (Apr 08 2021 at 13:44):But I side with Mike on the point that one should not require unique names in a library and rather be able to use informative disambiguation mechanisms.
Michael Soegtrop (Apr 08 2021 at 13:45):rather be able to use informative disambiguation mechanisms.
full qualification is a form of that :-)
Michael Soegtrop (Apr 08 2021 at 13:45):OK, so let's drop my PR for later.
Matthieu Sozeau (Apr 08 2021 at 13:45):Right now it works well when you are developing your own library but even then for example extraction is not up to the task in general and can get confused
Matthieu Sozeau (Apr 08 2021 at 13:46):Yes, absolutely that's just the most extreme form :)
Michael Soegtrop (Apr 08 2021 at 13:46):Can then someone please tag #dd3c399d6c6c9275c3f4b9feee46925f8f415f49?
Mike Shulman (Apr 08 2021 at 13:51):I'm certainly open to adding some disambiguation to make things easier on users, if From can be modified to make that less verbose than full qualification.
Michael Soegtrop (Apr 08 2021 at 13:54):The main issue with From as is is that for top level files which have duplicates one cannot use "From HoTT Require File" but has to say "Require HoTT.File".
Michael Soegtrop (Apr 08 2021 at 13:54):If one could avoid to have duplicates of top level files, From might work reasonably well.
Mike Shulman (Apr 08 2021 at 14:15):Do you mean for the current implementation of From, or a hypothetical modification of it?
Mike Shulman (Apr 08 2021 at 14:15):I don't think we have very many top level files with duplicate names -- maybe just Tactics and Utf8?
Michael Soegtrop (Apr 08 2021 at 14:42):Indeed:
find . -name "*.v" -type f | awk -F/ '{ name=$NF } cnt[name]==1 { print name, fst[name]; } cnt[name] { print name, $0 } { fst[name]=$0; cnt[name]++ }' | sort | grep "^[^/]*/[^/]*/[^/]*$"
Tactics.v ./theories/Tactics.v
Utf8.v ./theories/Utf8.v
without the final grep you get a list of all duplicate files.
Mike Shulman (Apr 08 2021 at 15:46):So are you talking about the current From or a hypothetical one? We could certainly rename the toplevel Tactics and Utf8 if that would allow From to solve the problem; it seems reasonable to put them in Basics anyway.
Théo Zimmermann (Apr 08 2021 at 16:23):One thing that puzzles me in this discussion is that this change is not actually needed in the tagged version. If it ended being merged, it would still do the job even if that was after the tag / release.
Michael Soegtrop (Apr 09 2021 at 07:03):@Théo Zimmermann : the latest tag (V8.13.1) is not what should go into platform. The latest information from @Ali Caglayan is that we either use dd3c399d6c6c9275c3f4b9feee46925f8f415f49 or something later.
Michael Soegtrop (Apr 09 2021 at 07:04):@Ali Caglayan @Matthieu Sozeau : if you want HoTT in the Coq Platform 2021.02.1 I need a tag today before noon. Otherwise I will do a release without it, but likely the next release with additional packages will be in 4..6 weeks.
Théo Zimmermann (Apr 09 2021 at 07:26):What I meant is simply that this commit could have been tagged two days ago and all this debate about whether to fully qualify Require could have happened after. But what's done is done.
Michael Soegtrop (Apr 09 2021 at 07:34):Well it would have been especially nice for the HoTT school ... I didn't foresee that this is so controversial.
Théo Zimmermann (Apr 09 2021 at 07:36):My point is that it would have had the same usefulness if done after the release.
Michael Soegtrop (Apr 09 2021 at 07:37):Hmm OK, that I fail to see because signed installers are also nice for a school, but I guess this opportunity is gone now.
Ali Caglayan (Apr 09 2021 at 07:38):I'm not really sure what to do anymore
Théo Zimmermann (Apr 09 2021 at 07:38):Not necessarily gone yet but significantly impeded for sure.
Michael Soegtrop (Apr 09 2021 at 07:38):But in the end I need to learn not to do such things in a hurry.
Théo Zimmermann (Apr 09 2021 at 07:38):@Ali Caglayan Just tag the commit. It works, no?
Michael Soegtrop (Apr 09 2021 at 07:38):@Ali Caglayan : I need a tag.
Michael Soegtrop (Apr 09 2021 at 07:39):Or you say I shall use V8.13.1, but before you said I shall use something later.
Michael Soegtrop (Apr 09 2021 at 07:40):@Ali Caglayan : or do you mean, you are not sure if you should do the tag with or without the change?
Michael Soegtrop (Apr 09 2021 at 07:40):In that case I would say if there is doubt / controversy do it without.
Ali Caglayan (Apr 09 2021 at 07:40):Yeah it feels a bit unfortunate without the change
Ali Caglayan (Apr 09 2021 at 07:41):But then again we haven't fully reached a consensus on it
Théo Zimmermann (Apr 09 2021 at 07:41):What both of you seem to not see is that if the point of the change is that users can copy a file from the repo and run it with the platform, then this change will still work even if done after the release.
Michael Soegtrop (Apr 09 2021 at 07:41):I thought that thsi would be a non controversial no brainer change, but apparently it isn't, so this needs time to be discussed.
Théo Zimmermann (Apr 09 2021 at 07:41):The release does not need this to work.
Ali Caglayan (Apr 09 2021 at 07:41):I will do a tag for today's master
Michael Soegtrop (Apr 09 2021 at 07:42):@Théo Zimmermann : "banging my had against the desk" - you are absolutely right
Michael Soegtrop (Apr 09 2021 at 07:43):Indeed it even doesn't nee dto be merged - one can say people to get it from the PR branch
Ali Caglayan (Apr 09 2021 at 07:44):By the way I am a bit confused, is 8.13.2 a real version? Or is it an april fools joke?
Michael Soegtrop (Apr 09 2021 at 07:44):It is a real version.
Ali Caglayan (Apr 09 2021 at 07:44):I can't find a change log for it, and it was published on 1 Apr
Michael Soegtrop (Apr 09 2021 at 07:45):But there is anyway no good reason to tie HoTT versions tightly to Coq versions. Minor releases of Coq are usually compatible.
Michael Soegtrop (Apr 09 2021 at 07:45):I guess HoTT depends only on the major version of Coq. So you could have a HoTT 8.13.7 which is the 7th release of HoTT for Coq 8.13.
Michael Soegtrop (Apr 09 2021 at 07:46):So please ping me here when the tag is done. The clock is ticking ...
Ali Caglayan (Apr 09 2021 at 07:47):Ok I've created a tag
Ali Caglayan (Apr 09 2021 at 07:47):https://github.com/HoTT/HoTT/releases/tag/CoqPlatform.8.13.1
Ali Caglayan (Apr 09 2021 at 07:47):@Michael Soegtrop
Ali Caglayan (Apr 09 2021 at 07:52):OK I pointed my release to the tagged tar and update the checksum
Ali Caglayan (Apr 09 2021 at 07:52):Hopefully I haven't screwed anything up
Michael Soegtrop (Apr 09 2021 at 07:54):You mean in the opam file?
Michael Soegtrop (Apr 09 2021 at 07:57):The tag name is a bit odd, but technically it is OK.
Michael Soegtrop (Apr 09 2021 at 08:27):OK, CI is through, so I can start with my part ...
Ali Caglayan (Apr 09 2021 at 08:28):Yeah, I don't have too much choice with the versioning. We were sticking to coq releases for our version numbers. So making two releases on the same version becomes difficult. Perhaps it is time to have this conversation again and start numbering our releases.
Théo Zimmermann (Apr 09 2021 at 08:29):@Enrico Tassi Any reason why you didn't publish the GitHub release for the V8.13.2 tag?
Enrico Tassi (Apr 09 2021 at 08:29):I was waiting for the packages to show up
Théo Zimmermann (Apr 09 2021 at 08:29):I see thanks
Théo Zimmermann (Apr 09 2021 at 08:36):But if you want my opinion, you could have just published the release on GitHub with a comment saying that binary installers will eventually be provided by the next release of the Coq platform.
Théo Zimmermann (Apr 09 2021 at 08:36):Having published the GitHub release is useful to inform other packagers to update their version of Coq (e.g., Nix, Arch, etc.)
Michael Soegtrop (Apr 09 2021 at 08:56):OK, the Coq Platform CI for 2021.02.1 is running ...
Michael Soegtrop (Apr 09 2021 at 09:01):@Enrico Tassi : I expect the packages to be available for signing between 12:30 and 13:45 (Mac should be first, Windows takes longer)
Enrico Tassi (Apr 09 2021 at 09:13):great, just point me to the artifact page
Enrico Tassi (Apr 09 2021 at 09:14):I'll then forward the windows packages to inria's signing service
Matthieu Sozeau (Apr 09 2021 at 10:56):And I'll learn how to sign the mac one for good :)
Michael Soegtrop (Apr 09 2021 at 11:06):@Enrico Tassi @Matthieu Sozeau : the Mac OS installer is ready and can be downloaded here (https://github.com/coq/platform/runs/2304424919)
Michael Soegtrop (Apr 09 2021 at 11:07):Windows should be ready in 20..30 minutes
Michael Soegtrop (Apr 09 2021 at 11:08):@Enrico Tassi : what do I need to do for the snap package?
Michael Soegtrop (Apr 09 2021 at 11:09):And why does the snap package only take 20 minutes?
Enrico Tassi (Apr 09 2021 at 11:15):by default it only builds coq
Enrico Tassi (Apr 09 2021 at 11:15):can we skype 10 minutes?
Enrico Tassi (Apr 09 2021 at 11:15):I'll show you
Michael Soegtrop (Apr 09 2021 at 11:17):Yes, I am available 13:25. I will send you an invite via email.
Enrico Tassi (Apr 09 2021 at 11:17):I'm super busy, so it will work faster
Enrico Tassi (Apr 09 2021 at 11:17):https://rdv3.rendez-vous.renater.fr/platform-coq
Enrico Tassi (Apr 09 2021 at 11:47):@Matthieu Sozeau are you taking care of signing the mac installer? Did I understand it right?
Matthieu Sozeau (Apr 09 2021 at 11:47):Yes, I'm working on it this afternoon
Enrico Tassi (Apr 09 2021 at 11:47):great
Matthieu Sozeau (Apr 09 2021 at 11:48):I'm trying to figure out how to download the installer now, a direct wget doesn't work, any idea?
Michael Soegtrop (Apr 09 2021 at 11:48):A wget (https://github.com/coq/platform/suites/2456409472/artifacts/52730843) should work ...
Enrico Tassi (Apr 09 2021 at 11:48):I use scp to the osx worker, but wget from it works as well
Enrico Tassi (Apr 09 2021 at 11:49):if you use curl, don't forget -L, since GH bounces you a little
Matthieu Sozeau (Apr 09 2021 at 11:49):It just doesn't
Matthieu Sozeau (Apr 09 2021 at 11:50):Maybe there's an option to add
Michael Soegtrop (Apr 09 2021 at 11:51):Indeed, let me check ...
Michael Soegtrop (Apr 09 2021 at 11:52):I guess you need a browser.
Michael Soegtrop (Apr 09 2021 at 11:53):If your are on a console machine I would suggest to follow Enrico`s advice of downloding it locally and scp it again, but it is a largish file.
Matthieu Sozeau (Apr 09 2021 at 11:54):Yeah, I'm doing that now
Matthieu Sozeau (Apr 09 2021 at 11:54):~10 min is ok
Michael Soegtrop (Apr 09 2021 at 11:54):You have sufficient upstream bandwidth?
Michael Soegtrop (Apr 09 2021 at 11:54):OK
Emilio Jesús Gallego Arias (Apr 09 2021 at 11:58):Sorry folks I didn't get the problem with the From, would anyone be kind to summarize it?
Matthieu Sozeau (Apr 09 2021 at 12:00):Well, I'm on fiber and only slightly limited by the provider, so it's alright
Enrico Tassi (Apr 09 2021 at 12:02):Oh, last time I did rename the files by hand (for windows) and forgot to update coq.nsi to call the coq-platform_$V_$ARCH.exe
Enrico Tassi (Apr 09 2021 at 12:02):@Michael Soegtrop you should be in CC for the signature, you should receive their reply with the signed files as well
Michael Soegtrop (Apr 09 2021 at 12:07):Emilio Jesús Gallego Arias said:
Sorry folks I didn't get the problem with the
From, would anyone be kind to summarize it?
The issue is that From HoTT Require A. does not work if there is a module HoTT.A and a module HoTT.B.A and there is no kind of disambiguation one could do besides removing the From and writing Require HoTT.A.
Michael Soegtrop (Apr 09 2021 at 12:08):Since HoTT has such cases, one has to mix Requires with and without From, which is really ugly.
Michael Soegtrop (Apr 09 2021 at 12:09):The suggestions I discussed with @Mike Shulman were about what one can do so that one can just write From HoTT Require A.
Michael Soegtrop (Apr 09 2021 at 12:12):@Enrico Tassi : yes, I got the mail, so I will take care of the upload.
Michael Soegtrop (Apr 09 2021 at 13:04):@Matthieu Sozeau : I just did the tag and the release, so you can upload the Mac installer now.
Michael Soegtrop (Apr 09 2021 at 13:05):(https://github.com/coq/platform/releases/tag/2021.02.1)
Matthieu Sozeau (Apr 09 2021 at 13:11):Shall I use commit c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d or the latest ?
Matthieu Sozeau (Apr 09 2021 at 13:11):I have the c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d version ready to sign now
Michael Soegtrop (Apr 09 2021 at 13:11):The latest one just changes the online readme file - it has no influence on the installer.
Matthieu Sozeau (Apr 09 2021 at 13:12):Ok
Michael Soegtrop (Apr 09 2021 at 13:12):So it is fine to use c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d
Michael Soegtrop (Apr 09 2021 at 13:12):I did things in this order to save some time ...
Matthieu Sozeau (Apr 09 2021 at 13:16):Ok, perfect
Emilio Jesús Gallego Arias (Apr 09 2021 at 13:30):Thanks @Michael Soegtrop , the corresponding Coq bug is https://github.com/coq/coq/issues/9697 , but I am not sure if there is a second one also by @Guillaume Melquiond asking for From Foo Require .A.
Michael Soegtrop (Apr 09 2021 at 13:34):Isn't this issue about naming modules in the code, rather than in requires? Of cause one could have the same syntax in both cases and drop the From Syntax. But the proposal in https://github.com/coq/coq/issues/9697 suffers from the same issues as the From syntax - it can be ambiguous.
Michael Soegtrop (Apr 09 2021 at 13:35):Or put in another way, for Require the issue #9697 is solved with the From syntax.
Michael Soegtrop (Apr 09 2021 at 13:44):@Matthieu Sozeau : you are uploading the Mac installer?
Théo Zimmermann (Apr 09 2021 at 13:46):Did @Enrico Tassi send the Windows installers to Inria's DSI in the end?
Enrico Tassi (Apr 09 2021 at 13:46):yes
Théo Zimmermann (Apr 09 2021 at 13:48):OK great!
Théo Zimmermann (Apr 09 2021 at 13:49):Sometimes they answer quite quick, but this is almost the week-end, so not sure about this time.
Matthieu Sozeau (Apr 09 2021 at 15:11):Yes, I'm working on it. Quite an hectic day here, sorry :)
Michael Soegtrop (Apr 09 2021 at 17:23):@Enrico Tassi : I updated the snap package - worked nicely.
Enrico Tassi (Apr 09 2021 at 17:24):great!
Enrico Tassi (Apr 09 2021 at 17:24):(still no news from the signing...)
Michael Soegtrop (Apr 09 2021 at 17:25):Well, I should have dropped the Require discussion yesterday and get it done ...
Enrico Tassi (Apr 09 2021 at 17:39):@Michael Soegtrop apparently you updated the latest track, but not the 2021.02 one. I'll let you fix that, so that you find out how to do that in the UI.
Enrico Tassi (Apr 09 2021 at 17:40):(maybe you did, but forgot to hit "save", it happened to me before)
Enrico Tassi (Apr 09 2021 at 17:44):FTR, it seems we do have some users (185 to be exact):
Screenshot-from-2021-04-09-19-43-11.png
Enrico Tassi (Apr 09 2021 at 18:00):@Michael Soegtrop one thing I forgot to tell you: you should make a personal account on snapcraft.io and then give it the rights to manage the coq-prover package from the settings->dashbord (advanced) interface. The main reason is that the master account, the one I gave you the password to, is linked to a private mailing list here at inria, and if you need to reset the password that is not going to work for you, while for a personal account you can use your personal mail address.
Michael Soegtrop (Apr 09 2021 at 18:12):@Enrico Tassi : yes the save buttons are nasty. I will try again after dinner.
Matthieu Sozeau (Apr 09 2021 at 18:28):Damn, signing broke the package
Matthieu Sozeau (Apr 09 2021 at 18:30):It tries to find a non-existent coqide.exe ??
Matthieu Sozeau (Apr 09 2021 at 18:32):Hmm, maybe that's not it
Matthieu Sozeau (Apr 09 2021 at 18:40):Ah no, the coq-platform dmg is broken from the get go
Matthieu Sozeau (Apr 09 2021 at 18:41):Even if I explicitely open it it fails to launch
Matthieu Sozeau (Apr 09 2021 at 18:41):The Ressources/bin/coqide inside is fine though
Matthieu Sozeau (Apr 09 2021 at 18:43):Oh they are definitely not the same coqide files:
#!/bin/sh
-HERE=$(cd $(dirname $0); pwd)
-export PATH="${HERE}/../Resources/bin/:${PATH}"
-export LD_LIBRARY_PATH="${HERE}"
-export DYLD_LIBRARY_PATH="${HERE}"
-export GDK_PIXBUF_MODULE_FILE="${HERE}/../Resources/lib/gdk-pixbuf-2.0/2.10.0/loaders/loaders.cache"
-export XDG_DATA_HOME="${HERE}/../Resources/share"
-exec coqide
+
+# Check if $0 is a link
+if [ -L "$0" ]
+then
+ LINKTARGET="$(readlink "$0")"
+ # Check if $0 is a an absolute or relative link
+ if [[ "$LINKTARGET" == '/'* ]]
+ then
+ BINDIR="$(dirname "$LINKTARGET")"
+ else
+ BINDIR="$(dirname "$0")/$(dirname "$LINKTARGET")"
+ fi
+else
+ BINDIR="$(dirname "$0")"
+fi
+
+# Normalize path
+BINDIR="$(cd "$BINDIR" ; pwd)"
+ROOTDIR="$(cd "$BINDIR/.." ; pwd)"
+
+export PATH="${BINDIR}:${PATH}"
+
+# This setting is required to find the image file format handlers
+# Note: these docs are contradicting on the default path for the "loaders.cache" file
+# https://developer.gnome.org/gdk-pixbuf/stable/gdk-pixbuf-query-loaders.html
+# https://developer.gnome.org/gtk3/stable/gtk-running.html
+# Setting GTK_EXE_PREFIX to ROOTDIR and putting the file into lib/gtk-3.0/3.0.0/loaders.cache doesn't work.
+export GDK_PIXBUF_MODULE_FILE="${ROOTDIR}/lib/gdk-pixbuf-2.0/2.10.0/loaders/loaders.cache"
+
+# This setting is required to find the "Input Method" handlers
+# ToDo: the cache file links to locales, but we don't install locales
+# ToDo: the selection of input methods seems questionable (with MacPorts)
+# ToDo: not sure if this is needed at all on Mac (which should have its own IME)
+export GTK_IM_MODULE_FILE="${ROOTDIR}/lib/3.0/3.0.0/immodules.cache"
+
+# This setting is required to find the adwaita icon theme
+export XDG_DATA_HOME="${ROOTDIR}/share"
+
+exec ${BINDIR}/coqide.exe
The first is from a Platform 02.0 package the later from 02.1
Matthieu Sozeau (Apr 09 2021 at 18:44):And if I replace the one in 02.1 with the one in 02.0 it definitely works...
Matthieu Sozeau (Apr 09 2021 at 18:46):@Michael Soegtrop any idea why that happened?
Michael Soegtrop (Apr 09 2021 at 18:48):Hmm, I tested it and it did work. Let me check again
Michael Soegtrop (Apr 09 2021 at 18:49):Works for me
Matthieu Sozeau (Apr 09 2021 at 18:50):Indeed the scripts by enrico have been merged so make_macos installer should give the first output. I'm dumbfounded now
Matthieu Sozeau (Apr 09 2021 at 18:51):Can you check you indeed get the first version?
Michael Soegtrop (Apr 09 2021 at 18:51):I get the second and it works
Michael Soegtrop (Apr 09 2021 at 18:51):bin$ cat coqide
#!/bin/sh
# Check if $0 is a link
if [ -L "$0" ]
then
LINKTARGET="$(readlink "$0")"
# Check if $0 is a an absolute or relative link
if [[ "$LINKTARGET" == '/'* ]]
then
BINDIR="$(dirname "$LINKTARGET")"
else
BINDIR="$(dirname "$0")/$(dirname "$LINKTARGET")"
fi
else
BINDIR="$(dirname "$0")"
fi
# Normalize path
BINDIR="$(cd "$BINDIR" ; pwd)"
ROOTDIR="$(cd "$BINDIR/.." ; pwd)"
export PATH="${BINDIR}:${PATH}"
# This setting is required to find the image file format handlers
# Note: these docs are contradicting on the default path for the "loaders.cache" file
# https://developer.gnome.org/gdk-pixbuf/stable/gdk-pixbuf-query-loaders.html
# https://developer.gnome.org/gtk3/stable/gtk-running.html
# Setting GTK_EXE_PREFIX to ROOTDIR and putting the file into lib/gtk-3.0/3.0.0/loaders.cache doesn't work.
export GDK_PIXBUF_MODULE_FILE="${ROOTDIR}/lib/gdk-pixbuf-2.0/2.10.0/loaders/loaders.cache"
# This setting is required to find the "Input Method" handlers
# ToDo: the cache file links to locales, but we don't install locales
# ToDo: the selection of input methods seems questionable (with MacPorts)
# ToDo: not sure if this is needed at all on Mac (which should have its own IME)
export GTK_IM_MODULE_FILE="${ROOTDIR}/lib/3.0/3.0.0/immodules.cache"
# This setting is required to find the adwaita icon theme
export XDG_DATA_HOME="${ROOTDIR}/share"
exec ${BINDIR}/coqide.exe
bin$
Are you sure you're trying 02.1 and not something else?
Michael Soegtrop (Apr 09 2021 at 18:52):yes
Michael Soegtrop (Apr 09 2021 at 18:52):The old file was quiet different and in a different older (under MacOS)
Michael Soegtrop (Apr 09 2021 at 18:52):bin$ ./coqc --version
The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 9 2021 9:08:16 with OCaml 4.07.1
Well, maybe it's a MacOS issue then, I'm on 10.15.7
Michael Soegtrop (Apr 09 2021 at 18:53):Quick online call?
Matthieu Sozeau (Apr 09 2021 at 18:53):Sure
Michael Soegtrop (Apr 09 2021 at 18:53):I send you a link via email
Michael Soegtrop (Apr 09 2021 at 18:53):done
Michael Soegtrop (Apr 09 2021 at 19:30):@Enrico Tassi : regarding snap: I think I did hit save in the 2021.02 stream, but it restores to version 13 then. I did it 3 times - I can't find a way to update it.
Enrico Tassi (Apr 09 2021 at 19:30):sometimes there is a refresh problem
Enrico Tassi (Apr 09 2021 at 19:30):I see it updated
Enrico Tassi (Apr 09 2021 at 19:30):https://snapcraft.io/coq-prover
Michael Soegtrop (Apr 09 2021 at 19:31):OK I have to hit browser refresh manually ...
Michael Soegtrop (Apr 09 2021 at 19:31):They seem to have a problem with their page
Enrico Tassi (Apr 09 2021 at 19:31):yeah, there is but I guess
Enrico Tassi (Apr 09 2021 at 19:31):but I see the update in the page above, so I guess it is fine
Michael Soegtrop (Apr 09 2021 at 19:31):Regarding Mac: the signing messed up the DMG.
Michael Soegtrop (Apr 09 2021 at 19:32):It can't handle the symlink from MacOS to bin folder.
Michael Soegtrop (Apr 09 2021 at 19:32):So @Matthieu Sozeau and me copied the script and adjusted it to the different position
Michael Soegtrop (Apr 09 2021 at 19:33):There are two shell scripts now - not nice but should work.
Enrico Tassi (Apr 09 2021 at 19:33):I see, well, the usual last-minute hickup
Michael Soegtrop (Apr 09 2021 at 19:33):Yes. And don't use "cp -r" on Mac.
Michael Soegtrop (Apr 09 2021 at 19:34):The man page explicitly says that it is very unlikely that it does what you want :-P
Michael Soegtrop (Apr 09 2021 at 19:34):Recursive copy is "cp-R" on Mac.
Enrico Tassi (Apr 09 2021 at 19:34):If one day you find the name of the chief architect of the macos userland, I'd like to meet him (not really)
Michael Soegtrop (Apr 09 2021 at 19:35):Well macOS is older than Linux ...
Enrico Tassi (Apr 09 2021 at 19:35):X
Enrico Tassi (Apr 09 2021 at 19:35):the "unix" one
Michael Soegtrop (Apr 09 2021 at 19:35):It is a true descendent of SystemV
Michael Soegtrop (Apr 09 2021 at 19:36):Let me see what my ancient SystemV manual says ...
Enrico Tassi (Apr 09 2021 at 19:36):as far as I know, the userland is collage of tools picked from all the bsd variants... to maximamise the probablility something is off
Enrico Tassi (Apr 09 2021 at 19:37):And I'm sorry to say that, but today there is only one unix, so if you do it differently... you are looking for troubles
Matthieu Sozeau (Apr 09 2021 at 19:37):-R is better indeed, and anyway it was forgetting the README.html file which was a pity :)
Matthieu Sozeau (Apr 09 2021 at 19:38):It's nice to see a long list of packages there!
Enrico Tassi (Apr 09 2021 at 19:38):ah ah, posix says -R ;-)
Michael Soegtrop (Apr 09 2021 at 19:38):My SystemV manual says -R :-) Well compatibility is really difficult.
Enrico Tassi (Apr 09 2021 at 19:39):https://www.unix.com/man-page/posix/1p/cp/
Enrico Tassi (Apr 09 2021 at 19:39):remark the PROLOG section
Michael Soegtrop (Apr 09 2021 at 19:40):Yes. That's what I meant - it is not always MacOS to blame when things are not the same. But anyway it is a pitty that they are not the same.
Michael Soegtrop (Apr 09 2021 at 19:41):@Matthieu Sozeau and all the SPDX record links ...
Enrico Tassi (Apr 09 2021 at 19:41):What I mean in my troll message, was that the userspace of OSX was "crafted" when Linux was already there...
Michael Soegtrop (Apr 09 2021 at 19:42):Well but it mostly follows Posix and Unix, and this is older than Linux.
Michael Soegtrop (Apr 09 2021 at 19:42):Anyway, citing my son: happy or those who forget what cannot be changed anyway (citing some opera).
Michael Soegtrop (Apr 09 2021 at 19:43):I am off for today. Have a nice weekend!
Enrico Tassi (Apr 09 2021 at 19:44):With my academic hat on, I notice that posix does not have -r, but I guess you did not get an error ;-)
Enrico Tassi (Apr 09 2021 at 19:44):Yea, nice weeked, and thanks for the release.
Michael Soegtrop (Apr 09 2021 at 19:45):The Mac man page says:
COMPATIBILITY
Historic versions of the cp utility had a -r option. This implementation
supports that option; however, its use is strongly discouraged, as it does
not correctly copy special files, symbolic links, or fifo's.
Do you want me to write an announcement? Or maybe you can post one yourself as soon as windows is there?
Michael Soegtrop (Apr 09 2021 at 19:46):I would prefer if you do the announcement.
Michael Soegtrop (Apr 09 2021 at 19:46):Ciao.
Enrico Tassi (Apr 09 2021 at 19:46): Earlier versions of this standard included support for the -r option to copy file hierarchies. The -r option is historical practice on BSD
and BSD-derived systems. This option is no longer specified by POSIX.1-2008 but may be present in some implementations. The -R option was
added as a close synonym to the -r option, selected for consistency with all other options in this volume of POSIX.1-2008 that do recursive
directory descent.
The difference between -R and the removed -r option is in the treatment by cp of file types other than regular and directory. It was imple-
mentation-defined how the - option treated special files to allow both historical implementations and those that chose to support -r with
the same abilities as -R defined by this volume of POSIX.1-2008. The original -r flag, for historic reasons, did not handle special files
any differently from regular files, but always read the file and copied its contents. This had obvious problems in the presence of special
file types; for example, character devices, FIFOs, and sockets.
I'll upload the signed macos package tonight hopefully :)
Enrico Tassi (Apr 09 2021 at 19:47):This is crazy ;-)
Enrico Tassi (Apr 09 2021 at 19:47):Ok, but I'll then wait Monday
Matthieu Sozeau (Apr 09 2021 at 19:48):Indeed, you can see how being driven by compatibility concerns results in a quite confusing situation :)
Matthieu Sozeau (Apr 09 2021 at 19:49):Well, I mean in the next ~15 mins
Matthieu Sozeau (Apr 09 2021 at 19:50):We always underestimate how long this stuff takes... I though I would be done with install matters on tuesday....
Enrico Tassi (Apr 09 2021 at 19:50):When is the HoTT school?
Matthieu Sozeau (Apr 09 2021 at 19:51):Monday, starting using Coq on Tuesday
Enrico Tassi (Apr 09 2021 at 19:51):Plenty of advance then ;-)
Matthieu Sozeau (Apr 09 2021 at 19:51):But the school is fine, we already have the stripped down packages that work.
Enrico Tassi (Apr 09 2021 at 19:52):signed?
Matthieu Sozeau (Apr 09 2021 at 19:52):No
Enrico Tassi (Apr 09 2021 at 19:52):I was kidding
Enrico Tassi (Apr 09 2021 at 19:52):Have a nice WE!
Matthieu Sozeau (Apr 09 2021 at 19:52):Haha ;)
Matthieu Sozeau (Apr 09 2021 at 19:52):You too
Michael Soegtrop (Apr 10 2021 at 07:51):@Enrico Tassi @Matthieu Sozeau : should I upload the unsigned Windows uninstallers until we have signed ones (with a note). Unsigned Windows installers (unlike unsigned Windows kernel drivers or apps) are not that bad - Windows will just pop up a Window stating that the author is unknown.
Michael Soegtrop (Apr 10 2021 at 09:24):Matthieu Sozeau said:
We always underestimate how long this stuff takes... I though I would be done with install matters on tuesday....
I hope this will get better now. The issue is that there was one missing piece: the DMG installer and its signing. I expect that this machinery needs much less changes in the future and we can concentrate on the actual content. At least it should be possible to separate working on the machinery and on the content.
Enrico Tassi (Apr 10 2021 at 10:03):I'm fine with that
Matthieu Sozeau (Apr 10 2021 at 12:37):I'm fine with unsigned ones while we wait
Michael Soegtrop (Apr 10 2021 at 12:46):OK, I will upload them then and leave a note
Théo Zimmermann (Apr 10 2021 at 16:41):@Michael Soegtrop From my experience handling releases for Coq itself, I would advise:
Both recommendations are minor though.
Théo Zimmermann (Apr 12 2021 at 08:09):@Enrico Tassi Maybe you should ping the DSI?
Théo Zimmermann (Apr 12 2021 at 08:09):Also, it sounds like this is time to publish the 8.13.2 release on the GitHub repo.
Enrico Tassi (Apr 12 2021 at 08:10):Well, we sent the email at 1PM IIRC, on friday, let's give them 1 working day before pinging them.
Enrico Tassi (Apr 12 2021 at 08:11):For 8.13.2, done!
Michael Soegtrop (Apr 12 2021 at 08:12):@Théo Zimmermann : thanks, good hint! I guess it would be best to upfront call the output of CI "_unsigned" and remove that when it is signed.
Enrico Tassi (Apr 12 2021 at 08:52):I'm about to send this:
Dear Coq community,
the Coq development team is proud to announce the immediate
availability of the Coq Platform version 2021.02.1.
The Coq platform is a distribution of the Coq proof assistant together
with a selection of Coq libraries. It provides a set of scripts to
compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS,
Windows and many Linux distributions in a reliable way with consistent
results. See [1] for the project homepage, and [2] for the new
instructions for getting Coq.
This release is based on Coq 8.13.2 and provides binary installers
for Windows, MacOS and Linux. The next point releases, starting with
2021.02.2, will focus on including more Coq libraries (and no
breaking change).
Highlights for Coq 8.13.2:
- Fix crash when using vm_compute on an irreducible PArray.set
- Fix crash when loading .vo files containing a vm_compute
normalized primitive array
- Fix Ltac2.Array.init computational complexity
Highlights for the Coq Platform version 2021.02.1:
- DMG installer package for macOS
- Homotopy Type Theory library version 8.13
- The Verified Software Toolchain updated to 2.7.1
comments?
Théo Zimmermann (Apr 12 2021 at 08:58):Looks good but a few comments:
Théo Zimmermann (Apr 12 2021 at 08:58): Théo Zimmermann (Apr 12 2021 at 08:59): Michael Soegtrop (Apr 12 2021 at 09:13):I think the concentration on the scripts first and the installers later is a bit misleading. How about:
the Coq development team is proud to announce the immediate
availability of the Coq Platform version 2021.02.1, based on Coq 8.13.2.
The Coq platform is a distribution of the Coq proof assistant together
with a selection of Coq libraries. See [1] for the project homepage,
and [2] for the new instructions for getting Coq.
For expert users it provides a set of scripts to compile and install
OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and
many Linux distributions in a reliable and extensible way with consistent
results.
For beginners it provides easy to use binary installers for Windows, MacOS and Linux.
The next point releases, starting with 2021.02.2, will focus on including
more Coq libraries (and no breaking change).
Also I would wait until the signed installers are uploaded, unless there is a good reason for not waiting.
Théo Zimmermann (Apr 12 2021 at 09:16):Looks better indeed!
Théo Zimmermann (Apr 12 2021 at 09:16):The website is now updated to stop special-casing macOS.
Théo Zimmermann (Apr 12 2021 at 09:17):Or actually it will be when the last commit is deployed.
Enrico Tassi (Apr 12 2021 at 09:35):Dear Coq community,
the Coq development team is proud to announce the immediate
availability of the Coq Platform version 2021.02.1, based on Coq 8.13.2.
The Coq platform is a distribution of the Coq proof assistant together
with a selection of Coq libraries. See [1] for the project homepage, and [2]
for the new instructions for getting Coq.
For expert users it provides a set of scripts to compile and install
OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and
many Linux distributions in a reliable and extensible way with consistent results.
For beginners it provides easy to use binary installers for Windows, MacOS and Linux.
The next point releases, starting with 2021.02.2, will focus on including more
Coq libraries (and no breaking change).
Highlights for Coq 8.13.2:
- Fix crash when using vm_compute on an irreducible PArray.set
- Fix crash when loading .vo files containing a vm_compute
normalized primitive array
- Fix Ltac2.Array.init computational complexity
Highlights for the Coq Platform version 2021.02.1:
- DMG installer package for macOS
- Homotopy Type Theory library version 8.13
- The Verified Software Toolchain updated to 2.7.1
Best regards,
--
Enrico Tassi for the Coq Team
[1]: https://github.com/coq/platform
[2]: https://coq.inria.fr/download
Here the current text, I can surely wait to send it.
Michael Soegtrop (Apr 12 2021 at 09:39):Thanks!
Théo Zimmermann (Apr 12 2021 at 09:41):LGTM
Enrico Tassi (Apr 13 2021 at 09:51):The installers are there, shall I send it?
Théo Zimmermann (Apr 13 2021 at 09:54):Yes, though shouldn't it be announced on the website as well?
Michael Soegtrop (Apr 13 2021 at 10:02):Yes, please go ahead!
Enrico Tassi (Apr 13 2021 at 10:03):sent, but I'm a bit short in time for the website
Théo Zimmermann (Apr 13 2021 at 10:06):FWIW, Discourse cuts everything after ---. I've edited your post on Discourse to fix that.
Enrico Tassi (Apr 13 2021 at 14:45):I did not receive my message on coq-club nor on coqdev, but it is on discourse... is inria's zimbra broken? Did you receive the main on coq-club?
Michael Soegtrop (Apr 13 2021 at 14:53):I did receive it on Coq Club
Enrico Tassi (Apr 13 2021 at 14:59):ok, then it is my zimbra setup which tricked me. all good
Enrico Tassi (Apr 13 2021 at 14:59):I have the impression it did deduplicate the message... miracles...
Last updated: Jun 06 2023 at 22:01 UTC