Bas Spitters (Jun 14 2022 at 10:49): Bas Spitters (Jun 14 2022 at 10:49):I see a lot of cool stuff going on. Is there a high level description of how things should fit together?
E.g.:
https://github.com/coq-community/coq-nix-toolbox
Some very old discussions:
https://github.com/coq/coq/wiki/OPAM
Some newer ones:
https://github.com/coq/coq/wiki/DuneWG-2022
I'm probably looking in the wrong place, so please point me to the right one :-)
Emilio Jesús Gallego Arias (Jun 14 2022 at 11:06):Bas Spitters said:
I see a lot of cool stuff going on. Is there a high level description of how things should fit together?
Hi @Bas Spitters , actually indeed so far, as you point out, trying to describe and coordinate all the stuff that is going on has been so far a harder challenge than the work on the stuff itself.
Ideas on how to organize better are welcome!
Emilio Jesús Gallego Arias (Jun 14 2022 at 11:06):We are doing for now these online events
Emilio Jesús Gallego Arias (Jun 14 2022 at 11:07):that's helpful for people who can attend, but those out get lost, we should have a more central info point
Théo Zimmermann (Jun 14 2022 at 11:08):With respect to opam / Coq Nix Toolbox dichotomy, you can have a look at our Hydras & Co. paper for an example of using both in a complementary fashion (https://hal.archives-ouvertes.fr/hal-03404668).
Bas Spitters (Jun 14 2022 at 11:12):@Théo Zimmermann Thanks. Would you imagine similar infrastructure to work for the HoTT book/HoTT library?
@Ali Caglayan may also want to chime in.
Théo Zimmermann (Jun 14 2022 at 11:15):It would work, but the need might be less striking because the HoTT library (I don't know anything about the HoTT book) is only compatible with one Coq version at once and does not have reverse dependencies (as far as I am aware). Testing with several versions of dependencies and with reverse dependencies is where the Coq Nix Toolbox brings the most benefits.
Bas Spitters (Jun 14 2022 at 11:19):The book and the HoTT library are being kept in sync with a script:
https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBook.v
Potentially, one would like to use a similar script for unimath and also for the various hott-agda and cubical agda libraries.
Just in case, one would like to stress test Nix ;-)
Ali Caglayan (Jun 14 2022 at 11:22):What infrastructure work are we talking about for HoTT? Getting it working with Nix?
Ali Caglayan (Jun 14 2022 at 11:22):I don't think there will be any difficulty in doing that.
Ali Caglayan (Jun 14 2022 at 11:23):The sync with book stuff isn't something that is automated however. Its just a python script that is run once every few years.
Ali Caglayan (Jun 14 2022 at 11:24):I don't know if that requires special Nix support.
Ali Caglayan (Jun 14 2022 at 11:24):However you might be interested to know that HoTT is sitting in the coq-unvierse atm. And the HoTT part of coq-equations is even depending on it!
Bas Spitters (Jun 14 2022 at 12:39):@Ali Caglayan I mentioned the hott book as by analogy with the Hydra book, that Theo linked too.
Théo Zimmermann (Jun 14 2022 at 13:04):OK, I was not aware that there were Coq files in the book repository as well.
Ali Caglayan (Jun 14 2022 at 14:08):There are in fact Coq files in the Book repository: https://github.com/HoTT/book/tree/master/coq_introduction. But I don't think Bas was referring to those. He was talking about the files we have in HoTT/HoTT that link directly with definitions in the book. There is a python script that scans the latex files and then produces appropriate headers/sections in a v file which can be filled out by hand.
Bas Spitters (Nov 11 2022 at 13:28):Looking for something else, I noticed this thread again. Is there a better understanding of how Universe, opam and platform relate/should work together? Just curious... @Emilio Jesús Gallego Arias
Karl Palmskog (Nov 11 2022 at 13:37):I don't think the Universe will ever be directly connected to the Platform. A subset of Platform projects are expected to build well with Dune, and thus be in scope of Universe
Emilio Jesús Gallego Arias (Nov 11 2022 at 14:48):Bas Spitters said:
Looking for something else, I noticed this thread again. Is there a better understanding of how Universe, opam and platform relate/should work together? Just curious... Emilio Jesús Gallego Arias
In terms of packaging that's a bit unclear, but I think for developers the idea of universe is to be a core workspace
Emilio Jesús Gallego Arias (Nov 11 2022 at 14:48):in the sense that you can setup subsets of universe to work simultaneously in several projects
Emilio Jesús Gallego Arias (Nov 11 2022 at 14:48):this will require some tooling
Last updated: Apr 19 2024 at 00:02 UTC