Stream: Coq Platform devs & users

Topic: Coq-HoTT in the platform?


view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 12 2021 at 10:13):

@Matthieu Sozeau TTOMK it should be fine

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 12 2021 at 11:44):

Our current makefile set up does much more than build the library (documentation, proviola etc.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Mar 12 2021 at 12:07):

@Michael Soegtrop has created a version of the windows installer before for an earlier HoTT workshop.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 13 2021 at 12:56):

In order words, nothing much has changed

view this post on Zulip Bas Spitters (Mar 13 2021 at 13:16):

https://github.com/HoTT/HoTT/issues/1424

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 28 2021 at 10:25):

@Matthieu Sozeau : is this Coq platform based or does it work in a different way?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 14:46):

I'll try just following the README instructions on a custom installer and report :)

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 15:39):

Yes, I'm trying that

view this post on Zulip Michael Soegtrop (Mar 29 2021 at 15:54):

@Matthieu Sozeau : if you have time now, we can have a chat on this.

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 15:55):

I'm in a meeting, but maybe in about ~1hr?

view this post on Zulip 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 ;-)

view this post on Zulip Michael Soegtrop (Mar 29 2021 at 15:58):

@Enrico Tassi : are you also available around 7 PM?

view this post on Zulip Enrico Tassi (Mar 29 2021 at 15:58):

nope

view this post on Zulip 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 ...).

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 16:31):

I'm available now @Michael Soegtrop

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 18:43):

The CI worked! https://github.com/coq/platform/pull/97/checks?check_run_id=2220877237

view this post on Zulip 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!

view this post on Zulip Enrico Tassi (Mar 29 2021 at 19:38):

just rebase on top of https://github.com/coq/platform/pull/50

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 22:35):

Indeed I have them available in the OS X package I'm testing now

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 22:37):

Ah that changed with my rebase on #50, that might be it

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 22:43):

Otherwise everythings there and can be run (with a little bit of path fiddling)

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 06:40):

So what is left to do? Test it on Mac and Windows?

view this post on Zulip 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 :)

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 09:02):

Also, on MacOS, the installer missed a symlink that should be installed as well

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 09:03):

I guess it should be changed in create_installer_macos.sh

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 09:11):

Can I assume we have gnu sed installed?

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Mar 30 2021 at 09:18):

Be careful. If I remember correctly, brew installs sed as gsed.

view this post on Zulip Enrico Tassi (Mar 30 2021 at 09:40):

I believe both brew and ports call it gsed

view this post on Zulip 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")

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 09:45):

Yep, I'm using gsed all the time :)

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 10:08):

It's just a path change, I think that'll be fine

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 10:08):

I think I've got macos covered, now about windows and the snap package

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 10:09):

Did you manage to try a build for windows @Michael Soegtrop ?

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 30 2021 at 11:15):

https://github.com/HoTT/HoTT/pull/1431

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 11:18):

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?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 11:26):

You mean the VERBOSE=1 (V=1 in HoTT Makefiles I think)?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 11:28):

due to Print statements in some files.

view this post on Zulip Guillaume Melquiond (Mar 30 2021 at 11:29):

Is there a reason to keep these Print statements in the first place?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 11:30):

sometimes there is a Check also

view this post on Zulip Ali Caglayan (Mar 30 2021 at 11:30):

especially in the unit tests

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 30 2021 at 11:32):

but then you have to give a name to definition
and fill any evars

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Mar 30 2021 at 11:37):

No, the output of Check goes to stdout.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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 ?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:32):

@Matthieu Sozeau I am using linux and I would be able to test

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:32):

What should I do?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:32):

Cool, it's here: https://github.com/coq/platform/actions/runs/701471850

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:34):

I don't know snap though :)

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:39):

I don't see any instructions for snap there btw

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:39):

but I am doing it the usual snap way

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 30 2021 at 14:46):

I can try it out for you

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:47):

It also hangs when I write snap --version

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:47):

That doesn't look healthy

view this post on Zulip Enrico Tassi (Mar 30 2021 at 14:49):

do you have snapd running? which linux distro are you on?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:50):

I didn't know we have to have snapd running?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:50):

I am using ubuntu bionic

view this post on Zulip Ali Caglayan (Mar 30 2021 at 14:50):

I just installed snapd from ubuntu repos

view this post on Zulip Enrico Tassi (Mar 30 2021 at 14:50):

it install fine here, but it does not include HoTT

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:52):

That's curious :)

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:53):

Yep, I'll have a look

view this post on Zulip Enrico Tassi (Mar 30 2021 at 14:53):

zap -extent=i

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:54):

I just put extent=f ?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 14:58):

Let's try

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:29):

New snap package here: https://github.com/coq/platform/actions/runs/701849310

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:29):

With HoTT this time :)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:39):

Yes, it's all that's left

view this post on Zulip 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")

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 15:41):

@Enrico Tassi : any chance we get this signed by INRIA?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:43):

If we can get them signed that would be great indeed

view this post on Zulip Enrico Tassi (Mar 30 2021 at 15:53):

for macos we can sign it by ourselves (not notarize it, which even Inria cannot)

view this post on Zulip Enrico Tassi (Mar 30 2021 at 15:53):

Here the howto: https://github.com/coq/coq/wiki/SigningReleases

view this post on Zulip Enrico Tassi (Mar 30 2021 at 15:54):

you need to access the osx slave, you both have the right I believe

view this post on Zulip Enrico Tassi (Mar 30 2021 at 15:54):

but you need the certificate password, I can give you that in a private chat

view this post on Zulip Enrico Tassi (Mar 30 2021 at 15:55):

do you want to follow the procedure? (cause I've to go)

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:56):

Sure

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 15:57):

Thanks !

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 16:11):

Would you happen to have an apple dev account ? :)

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 16:20):

Notarization requires a bit of work it seems, but nothing impossible

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 16:21):

Hmm, ci.inria.fr seems really unstable...

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Mar 30 2021 at 16:37):

It looks like it would bring less confusion and be better for everyone.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 16:58):

That would be simpler indeed. I'm for it.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:05):

Does someone know how hoqidetop is started by CoqIDE?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:07):

Atm there is a script hoqide

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:08):

Not that I can see it ... Anyway a shell script won't work on Windows.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:08):

What might work is do the argument hacking with a _CoqProject file, as Théo suggested.

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:08):

ah then its probably generated by ./autogen.sh

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:10):

Require Import HoTT.Basics.

Check Contr.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:10):

Here is one: https://github.com/HoTT/EPIT-2020/pull/2/files#diff-3110edd8b78b8e325fdeee6f017dd26ca7a2a3a5ca318427a34477e52ee7c6b3

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:11):

OK, then I think we should provide a _CoqProject file for users which sets these arguments

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:11):

Let me try the _CoqProject approach ...

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:11):

Ah, I didn't think of that, indeed that's good!

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:11):

This is exactly what https://github.com/HoTT/HoTT/pull/1431 does

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:13):

Ah I see what you mean now

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:13):

I think one can get around all the hoqxyz files with a simple _CoqProject file.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:14):

Give me a few minutes ...

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:22):

@Matthieu Sozeau : the ... in the path are supposed to refer to the Coq root folder?

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:24):

This doesn't seem to work.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:28):

Yes, I was refering to the absolute paths

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:28):

Great!

view this post on Zulip 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.)

view this post on Zulip 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)

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

But we still need the Coqlib option and -indices-matter or not?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:30):

And the coqlib will disappear as well I believe

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:30):

Just -indices-matter

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

I see.

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

This solves the path issue.

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

Will this be merged early enough before the workshop?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:30):

I merged my PR upstream, you should be able to use coqide with HoTT np

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:31):

Ah, it is already merged? We just need to update the opam package?

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:31):

Cool. Can you make a point release for Coq-8.13?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:31):

HoTT passes two important flags to coq -noinit and indices-matter

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:31):

Ah, the -noinit replaces the -coqlib?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:32):

yep

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:32):

nice.

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:33):

I'll make an opam release for 13.1

view this post on Zulip 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-matter

and remove all teh hoq files?

Exactly.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:33):

We can take a local opam patch file in the platform

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:34):

(for the time beeing)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:36):

I tend to do it that way for new stuff.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:36):

If it all works as expected, we can still push it to the opam repo.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:37):

As you prefer then

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:39):

If you have time now, go ahead, otherwise I'll work on it tomorrow morning

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:39):

OK, then I will do it now.

view this post on Zulip Matthieu Sozeau (Mar 30 2021 at 17:39):

Cool, thanks everyone!

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:41):

67cdb33f91a1fba2f4d8413757ab9813c2652bf4

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:41):

but I am working on a release with a tag and an opam release

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:42):

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).

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:42):

at least just the vo files

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:43):

I would prefer to wait with the release until we tested it in the platform

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:43):

if you want to build documentation etc you still have to use the old makefile

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:43):

Can you send me the build and install instructions you would recommend?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:45):

this ofcourse requires coq_makefile to be around

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:45):

coq_makefile is part of teh coq opam package

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:45):

so it should be fine?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:46):

I think I will do the opam release with this build method btw

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:46):

but the "official" build instructions on the repo still suggest using the old makefile

view this post on Zulip Ali Caglayan (Mar 30 2021 at 17:46):

I just haven't had the time to update this yet

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 17:46):

As I said, let's test it and see ...

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:00):

OK, a local Windows build is running ...

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 30 2021 at 18:50):

@Michael Soegtrop my opam build seems to be successful. How is your testing going?

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:50):

M ylocal build works as expected with a _CoqProject file.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:50):

I push to @Matthieu Sozeau PR branch to run CI.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:51):

We can compare our opam files then.

view this post on Zulip 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"
}

view this post on Zulip Ali Caglayan (Mar 30 2021 at 18:53):

I made a V8.13.1 tag for the HoTT library btw

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:53):

For performance reasons it is prefered to use tar.gz files for releases.

view this post on Zulip 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"
}

view this post on Zulip Ali Caglayan (Mar 30 2021 at 18:55):

Ah I wasn't aware of this

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:58):

So all in all it is pretty nice now!

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 18:58):

I guess you know how to compute the SHA code ...

view this post on Zulip Ali Caglayan (Mar 30 2021 at 18:59):

No not really. How do you do it?

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 19:01):

view this post on Zulip Ali Caglayan (Mar 30 2021 at 19:02):

Stupid question: What's the point of a checksum here?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 30 2021 at 19:05):

I am gone for today! LetÄs continue tomorrow. What timezone are you in?

view this post on Zulip Ali Caglayan (Mar 30 2021 at 20:18):

@Michael Soegtrop I'm in Europe time

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 07:02):

Btw.: is it possible to sneak into some introductory lectures on HoTT?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 07:37):

Hello! Great news! I can just rebase interactively and remove the unneeded stuff

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 07:38):

@Ali Caglayan you mean the opam package?

view this post on Zulip Ali Caglayan (Mar 31 2021 at 07:38):

Yes, sorry, still waking up :-)

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 07:49):

I think we should give a logical name to contrib/, e.g. HoTT.contrib

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:03):

The thing is it gets installed in user-contrib/'', which is clearly wrong

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:04):

@Enrico Tassi @Michael Soegtrop If you can make it happen that'd be great :)

view this post on Zulip Ali Caglayan (Mar 31 2021 at 08:16):

I think we should then update the install step not to install things from contrib

view this post on Zulip Ali Caglayan (Mar 31 2021 at 08:17):

currently it is the default makefile install

view this post on Zulip Ali Caglayan (Mar 31 2021 at 08:17):

But I don't know how to blacklist things from being installed there

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:54):

Most of the files get installed right, but the two in contrib/ are problematic

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:54):

Locally, I see them get installed in lib/coq/user-contrib/''

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 08:57):

I see, I can check later in Windows around noon.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 09:05):

Ok, that's fine. I'm sure I can find somewhere to host them.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 09:09):

@Michael Soegtrop We already have tags: [ "logpath:HoTT" ] btw

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 09:10):

Yeah, this isn't our main setup yet

view this post on Zulip Ali Caglayan (Mar 31 2021 at 09:10):

I am working on untangling our current makefile

view this post on Zulip Ali Caglayan (Mar 31 2021 at 09:10):

Eventually that will call the one generated by coq_makefile

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 09:16):

OK I have squashed the commits

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:16):

Yeah, so passing -boot makes things much more complicated here

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:17):

I need to then explicitly find the ltac and numeral notations plugin

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:17):

or at least get _CoqProject to point to them

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:17):

in my testing, everything was working fine without the flag

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 17:18):

I see, you want to keep only the -I part

view this post on Zulip 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

view this post on Zulip 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/'' ?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 17:20):

(deleted)

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:20):

@Michael Soegtrop Yes, I'm taking a look now

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 17:27):

Just move it to released and remove the .dev extension.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:30):

Yeah, I can do a release for that

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:30):

let me get the changes to _CoqProject sorted first

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 17:30):

But lets' wait until everything is nice and clean in Coq platform.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:39):

OK just checking nothing is breaking: https://github.com/HoTT/HoTT/pull/1433

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:42):

my local tests seem to indicate it is working as expected

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 17:45):

Contrib sounds more like "stuff you might want to look at much later".

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 17:50):

Then I suggest we use a separete _ContribProject file and forget about it when we install

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:51):

How does that work?

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:52):

You can think of the files in Contrib as almost being documentation

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:56):

anyhow, I think keeping the files in HoTT.Contrib is fine for now

view this post on Zulip Ali Caglayan (Mar 31 2021 at 17:56):

doing what mattieu suggests will complicate things on our end for now

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 17:58):

Ah OK, I thought this was a nice tutorial on HoTT users would like to find.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:00):

OK. If users are not supposed to find them easily, HoTT.Contrib is just fine.

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:01):

Then of cause there is also no need to make them run from CoqIDE.

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:01):

(easily)

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:01):

speaking of CoqIDE, did you test HoTT with it?

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:01):

I got it working yesterday, but today I am having trouble

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:02):

Yes, sure. Works fine as long as you have a _CoqProject file with the two options.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:02):

Just tested it now, it's working again

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:02):

earlier it was getting confused with Coq.Init.Prelude

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:03):

It reads the _CoqProject file only on file open.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:03):

yes, I suspected as much

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:03):

Also stuff in scratch buffers won't work.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:04):

scratch buffers seem to work for me

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:04):

but I am running from the _CoqProject directory so maybe thats why

view this post on Zulip Michael Soegtrop (Mar 31 2021 at 18:04):

Possibly.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 31 2021 at 18:36):

@Michael Soegtrop Alright how is this: https://github.com/coq/opam-coq-archive/pull/1671

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 01 2021 at 07:53):

@Enrico Tassi : sounds good, so let#s plan for that.

view this post on Zulip Ali Caglayan (Apr 01 2021 at 15:13):

@Michael Soegtrop I should be available over Easter

view this post on Zulip Michael Soegtrop (Apr 01 2021 at 17:22):

@Ali Caglayan : good - I will ping you here every now and again ...

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 06 2021 at 21:13):

dd3c399d6c6c9275c3f4b9feee46925f8f415f49

view this post on Zulip Ali Caglayan (Apr 06 2021 at 21:14):

https://github.com/HoTT/HoTT/blob/master/theories/Homotopy/BlakersMassey.v

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 06:38):

@Matthieu Sozeau : not yet, but likely around noon - the installers will be unsigned, though.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 07:07):

I picked theories/Analysis/Locator.v.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 07:59):

I think that's fair to ask for cleanly qualified names in a library.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:19):

Maybe the From HoTT Require ... syntax helps to keep the require statements readable.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:20):

Ah ok, so this causes problems outside of the library

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:20):

Jason has a script that can qualify modules IIRC

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:26):

So under the line this improves the situation for HoTT learners considerably.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:30):

Actually From ... Require has -R semantics.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 HoTT everywhere 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.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:40):

Eugh, some of our files already have the HoTT qualification which makes my life harder

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:41):

I'll try one more thing first

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:47):

Let me check. Which file are you at?

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:48):

Categories/GroupoidCategory/Morphisms.v for example

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:48):

So now I would have to split those up...

view this post on Zulip 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.

view this post on Zulip 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' {} \;

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:50):

Not sure if this is going to work ...

view this post on Zulip Ali Caglayan (Apr 07 2021 at 08:51):

Yeah it doesn't :sweat_smile:

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:55):

It is indeed nasty because you have so many duplicate names

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:56):

I guess one needs to look into the .d files to get this sorted out.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 07 2021 at 08:58):

Wouldn't From HoTT Require Category.Core work in this case?

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 08:58):

Ah yes ...

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:00):

Yeah typically with names like Core they will be qualified as they appear in a lot of places in the library.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 09:03):

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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:07):

I like the idea of having a From HoTT. statement that sets the default form.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 09:09):

But I guess it wouldn't work for the level of complexity you have in HoTT.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 09:22):

So how shall we proceed? Do you have the scripts from Jason you mentioned?

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:28):

I think I am misremembering then

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:29):

I can't find Jason's scripts

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:29):

I can only find one which minimizes requires and imports

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:31):

Oh no it exists

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:32):

https://coq.inria.fr/related-tools.html

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:32):

at the bottom

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:32):

https://github.com/JasonGross/coq-tools/blob/master/move-requires.py

view this post on Zulip Ali Caglayan (Apr 07 2021 at 09:33):

There are quite a few scripts there that might be useful

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 09:33):

Looks too simple to be likely to work.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 09:51):

Yup. I dream of a day where we can program such things in MetaCoq :)

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 09:51):

Just load the .vos, crawl the environment and output the minimal dependencies for each file

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 10:08):

I'm not having much success with Jason's scripts

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 10:47):

@Ali Caglayan : I expected that. If you want I can have a look at it.

view this post on Zulip Ali Caglayan (Apr 07 2021 at 10:48):

That would be great

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 10:48):

OK, after lunch ...

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 10:50):

(I used a local HoTT opam file in the patch repo).

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 12:04):

Great news!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 16:17):

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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 16:58):

FWIW, I can run HoTT on the provided MacOS Installer from the CI just fine

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:00):

Indeed, that could happen

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 17:01):

So especially for a HoTT school one might want to change this.

view this post on Zulip Michael Soegtrop (Apr 07 2021 at 17:01):

Applying Jason's script as above fixes this.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip Ali Caglayan (Apr 07 2021 at 17:20):

I'll try and do a PR later

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:27):

I'm fine with it!

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 09:17):

Sorry I didn't have the time for it, I can quickly do it now

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 09:30):

OK. I can take care of the opam packages as soon as you have a tag.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 09:35):

The script is taking some time to run!

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:00):

Ah the way you called the script caused Basics to get extended to Coq.Program.Basics

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:00):

I need to set the coqc and try again

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:01):

It took roughly half an hour to finish it last time

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:18):

I also need it to stop crawling in the coq submodule

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:18):

That seems to have imporved the timing

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:45):

I really didn't think about building the library first...

view this post on Zulip Ali Caglayan (Apr 08 2021 at 10:45):

But now it looks like it has worked I will crate a PR

view this post on Zulip Gaëtan Gilbert (Apr 08 2021 at 11:00):

Why doesn't -R theories HoTT in the coqproject work?

view this post on Zulip Ali Caglayan (Apr 08 2021 at 11:00):

@Gaëtan Gilbert Can I have some more context?

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Ali Caglayan (Apr 08 2021 at 11:13):

So it seems there is a correct _CoqProject but it still doesn't work

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Apr 08 2021 at 11:17):

It could be

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 11:56):

@Ali Caglayan : let me just do a PR for that.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:03):

Actually it takes less than 1 second to run ...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:11):

@Ali Caglayan : https://github.com/HoTT/HoTT/pull/1445

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:12):

@Michael Soegtrop I already had a PR up: https://github.com/HoTT/HoTT/pull/1444

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:13):

Sorry if I didn't make it clear, I managed to get the script to work

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:14):

Yes, I hadn't built the library first

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:15):

It runs in under a second like you said

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:15):

Sorry, I didn't read the last lines of your comment.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:15):

I'm actually going to close my PR since something got broken along the way

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:16):

OK, I reopen mine then ...

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:17):

Sorry about athat

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:17):

No issue. I will put a few comments into mine how it was done (for reference).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 08 2021 at 12:22):

use the hoq scripts, otherwise you won't get -indices-matter etc

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:23):

Well not gone as of yet, but not necessary to build the library

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:24):

@Ali Caglayan : afaik the opam package does not install them.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:24):

Yes, but using the hoq scripts is still the recommended method in the git repo

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:24):

I just haven't gotten round to doing that change yet

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:25):

OK. I was talking about what is in Opam / the Coq Platform.

view this post on Zulip Ali Caglayan (Apr 08 2021 at 12:26):

Yep, I was just making sure everybody knew what was happening :-)

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:30):

So let me summarize, since the discussion took a few turns:

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:31):

And yes, one still needs a _CoqProject file, but it contains only the two -arg options.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:35):

Right

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:36):

This is nothing specific to HoTT.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:37):

So really what we are doing is working around broken behavior of macOS?

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:37):

@Mike Shulman : no. The files are not easy to find under .opam in Linux either.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:38):

You won't find them unless you know very well where to look.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:41):

Well I would say that with all the duplicate names, it does make it easier.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:41):

We generally already qualify duplicate names.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:41):

Sufficiently to disambiguate.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:44):

Is that just because of duplicate names?

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:45):

The problem with From comes from duplicate names, yes.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:45):

Things like HoTT.A and HoTT.B.A.

view this post on Zulip 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.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:48):

Isn't the "tail" precisely what a relative path name does?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:49):

Even though C/D.v is the "tail" and I've omitted the "head" A/B.

view this post on Zulip Mike Shulman (Apr 08 2021 at 12:49):

Are you saying that your students don't understand relative path names either?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:54):

Other libraries generally do not have duplicated names.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 12:54):

I would say HoTT as pretty much at the extreme end of having duplicate names.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 Lib associates 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mike Shulman (Apr 08 2021 at 13:18):

I still maintain that something is wrong with that.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 13:45):

rather be able to use informative disambiguation mechanisms.

full qualification is a form of that :-)

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 13:45):

OK, so let's drop my PR for later.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 13:46):

Yes, absolutely that's just the most extreme form :)

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 13:46):

Can then someone please tag #dd3c399d6c6c9275c3f4b9feee46925f8f415f49?

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip Michael Soegtrop (Apr 08 2021 at 13:54):

If one could avoid to have duplicates of top level files, From might work reasonably well.

view this post on Zulip Mike Shulman (Apr 08 2021 at 14:15):

Do you mean for the current implementation of From, or a hypothetical modification of it?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:38):

I'm not really sure what to do anymore

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 07:38):

Not necessarily gone yet but significantly impeded for sure.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:38):

But in the end I need to learn not to do such things in a hurry.

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 07:38):

@Ali Caglayan Just tag the commit. It works, no?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:38):

@Ali Caglayan : I need a tag.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:40):

In that case I would say if there is doubt / controversy do it without.

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:40):

Yeah it feels a bit unfortunate without the change

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:41):

But then again we haven't fully reached a consensus on it

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 07:41):

The release does not need this to work.

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:41):

I will do a tag for today's master

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:42):

@Théo Zimmermann : "banging my had against the desk" - you are absolutely right

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:44):

It is a real version.

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:44):

I can't find a change log for it, and it was published on 1 Apr

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:46):

So please ping me here when the tag is done. The clock is ticking ...

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:47):

Ok I've created a tag

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:47):

https://github.com/HoTT/HoTT/releases/tag/CoqPlatform.8.13.1

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:47):

@Michael Soegtrop

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:52):

OK I pointed my release to the tagged tar and update the checksum

view this post on Zulip Ali Caglayan (Apr 09 2021 at 07:52):

Hopefully I haven't screwed anything up

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:54):

You mean in the opam file?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 07:57):

The tag name is a bit odd, but technically it is OK.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 08:27):

OK, CI is through, so I can start with my part ...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Apr 09 2021 at 08:29):

I was waiting for the packages to show up

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 08:29):

I see thanks

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 08:56):

OK, the Coq Platform CI for 2021.02.1 is running ...

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Apr 09 2021 at 09:13):

great, just point me to the artifact page

view this post on Zulip Enrico Tassi (Apr 09 2021 at 09:14):

I'll then forward the windows packages to inria's signing service

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 10:56):

And I'll learn how to sign the mac one for good :)

view this post on Zulip 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)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:07):

Windows should be ready in 20..30 minutes

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:08):

@Enrico Tassi : what do I need to do for the snap package?

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

And why does the snap package only take 20 minutes?

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:15):

by default it only builds coq

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:15):

can we skype 10 minutes?

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:15):

I'll show you

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:17):

Yes, I am available 13:25. I will send you an invite via email.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:17):

I'm super busy, so it will work faster

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:17):

https://rdv3.rendez-vous.renater.fr/platform-coq

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:47):

@Matthieu Sozeau are you taking care of signing the mac installer? Did I understand it right?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 11:47):

Yes, I'm working on it this afternoon

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:47):

great

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:48):

A wget (https://github.com/coq/platform/suites/2456409472/artifacts/52730843) should work ...

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:48):

I use scp to the osx worker, but wget from it works as well

view this post on Zulip Enrico Tassi (Apr 09 2021 at 11:49):

if you use curl, don't forget -L, since GH bounces you a little

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 11:49):

It just doesn't

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 11:50):

Maybe there's an option to add

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:51):

Indeed, let me check ...

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:52):

I guess you need a browser.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 11:54):

Yeah, I'm doing that now

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 11:54):

~10 min is ok

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:54):

You have sufficient upstream bandwidth?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 11:54):

OK

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 12:00):

Well, I'm on fiber and only slightly limited by the provider, so it's alright

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 12:12):

@Enrico Tassi : yes, I got the mail, so I will take care of the upload.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:05):

(https://github.com/coq/platform/releases/tag/2021.02.1)

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 13:11):

Shall I use commit c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d or the latest ?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 13:11):

I have the c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d version ready to sign now

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:11):

The latest one just changes the online readme file - it has no influence on the installer.

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 13:12):

Ok

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:12):

So it is fine to use c41cf7dc9607833702213fd7bc8dfc0ce1d0e14d

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:12):

I did things in this order to save some time ...

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 13:16):

Ok, perfect

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:35):

Or put in another way, for Require the issue #9697 is solved with the From syntax.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:44):

@Matthieu Sozeau : you are uploading the Mac installer?

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 13:46):

Did @Enrico Tassi send the Windows installers to Inria's DSI in the end?

view this post on Zulip Enrico Tassi (Apr 09 2021 at 13:46):

yes

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 13:48):

OK great!

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 15:11):

Yes, I'm working on it. Quite an hectic day here, sorry :)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 17:23):

@Enrico Tassi : I updated the snap package - worked nicely.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 17:24):

great!

view this post on Zulip Enrico Tassi (Apr 09 2021 at 17:24):

(still no news from the signing...)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 17:25):

Well, I should have dropped the Require discussion yesterday and get it done ...

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 17:40):

(maybe you did, but forgot to hit "save", it happened to me before)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:12):

@Enrico Tassi : yes the save buttons are nasty. I will try again after dinner.

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:28):

Damn, signing broke the package

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:30):

It tries to find a non-existent coqide.exe ??

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:32):

Hmm, maybe that's not it

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:40):

Ah no, the coq-platform dmg is broken from the get go

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:41):

Even if I explicitely open it it fails to launch

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:41):

The Ressources/bin/coqide inside is fine though

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:43):

The first is from a Platform 02.0 package the later from 02.1

view this post on Zulip 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...

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:46):

@Michael Soegtrop any idea why that happened?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:48):

Hmm, I tested it and it did work. Let me check again

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:49):

Works for me

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:51):

Can you check you indeed get the first version?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:51):

I get the second and it works

view this post on Zulip 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$

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:52):

Are you sure you're trying 02.1 and not something else?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:52):

yes

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:52):

The old file was quiet different and in a different older (under MacOS)

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:53):

Well, maybe it's a MacOS issue then, I'm on 10.15.7

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:53):

Quick online call?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 18:53):

Sure

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:53):

I send you a link via email

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 18:53):

done

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:30):

sometimes there is a refresh problem

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:30):

I see it updated

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:30):

https://snapcraft.io/coq-prover

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:31):

OK I have to hit browser refresh manually ...

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:31):

They seem to have a problem with their page

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:31):

yeah, there is but I guess

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:31):

but I see the update in the page above, so I guess it is fine

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:31):

Regarding Mac: the signing messed up the DMG.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:32):

It can't handle the symlink from MacOS to bin folder.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:32):

So @Matthieu Sozeau and me copied the script and adjusted it to the different position

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:33):

There are two shell scripts now - not nice but should work.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:33):

I see, well, the usual last-minute hickup

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:33):

Yes. And don't use "cp -r" on Mac.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:34):

Recursive copy is "cp-R" on Mac.

view this post on Zulip 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)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:35):

Well macOS is older than Linux ...

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:35):

X

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:35):

the "unix" one

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:35):

It is a true descendent of SystemV

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:36):

Let me see what my ancient SystemV manual says ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:38):

It's nice to see a long list of packages there!

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:38):

ah ah, posix says -R ;-)

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:38):

My SystemV manual says -R :-) Well compatibility is really difficult.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:39):

https://www.unix.com/man-page/posix/1p/cp/

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:39):

remark the PROLOG section

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:41):

@Matthieu Sozeau and all the SPDX record links ...

view this post on Zulip 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...

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:42):

Well but it mostly follows Posix and Unix, and this is older than Linux.

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:43):

I am off for today. Have a nice weekend!

view this post on Zulip 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 ;-)

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:44):

Yea, nice weeked, and thanks for the release.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:45):

Do you want me to write an announcement? Or maybe you can post one yourself as soon as windows is there?

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:46):

I would prefer if you do the announcement.

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 19:46):

Ciao.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:47):

I'll upload the signed macos package tonight hopefully :)

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:47):

This is crazy ;-)

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:47):

Ok, but I'll then wait Monday

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:48):

Indeed, you can see how being driven by compatibility concerns results in a quite confusing situation :)

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:49):

Well, I mean in the next ~15 mins

view this post on Zulip 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....

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:50):

When is the HoTT school?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:51):

Monday, starting using Coq on Tuesday

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:51):

Plenty of advance then ;-)

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:51):

But the school is fine, we already have the stripped down packages that work.

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:52):

signed?

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:52):

No

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:52):

I was kidding

view this post on Zulip Enrico Tassi (Apr 09 2021 at 19:52):

Have a nice WE!

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:52):

Haha ;)

view this post on Zulip Matthieu Sozeau (Apr 09 2021 at 19:52):

You too

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 10 2021 at 10:03):

I'm fine with that

view this post on Zulip Matthieu Sozeau (Apr 10 2021 at 12:37):

I'm fine with unsigned ones while we wait

view this post on Zulip Michael Soegtrop (Apr 10 2021 at 12:46):

OK, I will upload them then and leave a note

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 08:09):

@Enrico Tassi Maybe you should ping the DSI?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 12 2021 at 08:11):

For 8.13.2, done!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 08:58):

Looks good but a few comments:

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 08:58):

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 08:59):

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 09:16):

Looks better indeed!

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 09:16):

The website is now updated to stop special-casing macOS.

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 09:17):

Or actually it will be when the last commit is deployed.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 12 2021 at 09:39):

Thanks!

view this post on Zulip Théo Zimmermann (Apr 12 2021 at 09:41):

LGTM

view this post on Zulip Enrico Tassi (Apr 13 2021 at 09:51):

The installers are there, shall I send it?

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:54):

Yes, though shouldn't it be announced on the website as well?

view this post on Zulip Michael Soegtrop (Apr 13 2021 at 10:02):

Yes, please go ahead!

view this post on Zulip Enrico Tassi (Apr 13 2021 at 10:03):

sent, but I'm a bit short in time for the website

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 10:06):

FWIW, Discourse cuts everything after ---. I've edited your post on Discourse to fix that.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 13 2021 at 14:53):

I did receive it on Coq Club

view this post on Zulip Enrico Tassi (Apr 13 2021 at 14:59):

ok, then it is my zimbra setup which tricked me. all good

view this post on Zulip Enrico Tassi (Apr 13 2021 at 14:59):

I have the impression it did deduplicate the message... miracles...


Last updated: Jan 29 2023 at 19:02 UTC