Julien Lepiller <jul...@lepiller.eu> writes: > OCaml stuff can easily be imported with guix import opam. I know coq > packages use a separate opam repository, so it would be nice if the > importer could take an optional parameter to indicate a custom opam > repository url. I'm not sure the coq repo is converted to opam 2 yet > though.
To my knowledge the Coq repo is not compliant with OPAM 2 quite yet. Maybe this has changed since I last checked, but I would be more than happy to ask upstream if this is still the case. I think working on an importer for those modified OPAM->Coq packages would be a fantastic start to that problem. > I can see the benefits of formal methods and benefits of guix, but > what does guix provide or could provide to formal method people > specifically? Is it "only" the nice guarantees it gives to any > programer, or is there something else? Maybe the question is why does > it matter more to fm people than to other programmers? I think it is a combination of what every other programmer is offered, and the possibilities offered by what bootstrapping has to offer for creating a machine from "nothing". There is still a lot of unknowns here, but I speculate that there is definitely more to be found as the concept progresses. I think your question is valid, and should likely be a central thesis to the working group; "What does Guix offer to the formal methods community that it could specifically benefit from?" > I think we're still a small community, so we can continue talking > about it on the main channel. We're trying to avoid dividing > information, that's why we allow any language on tge channel, instead > of having separate chans for each language. We also always hear about > bootstrapping or the hpc effort on the main channel. Let's talk about > fm :). You can count me in. Agreed, lets not separate the community. Keep the communication integrated. Though, I wonder if maybe I could draft an article for the Guix website blog; or maybe we could organize our goals somewhere? I am not quite sure what the best option here is. For example, one of the goals is a possible bootstrapping compiler for ML that I mentioned before, that would be dedicated to the GNU project in a similar fashion to Jan's GNU Mes (which, thank you Jan for the supportive messages). Combine this on maybe working out a bootstrap for OCaml, creating an importer for Coq, working on some more programming research-related questions in the context of Guix and suddenly we have ourselves a trifecta of big questions that need to be articulated _somewhere_ so we can retain some scope. Maybe Guix needs a wiki similar to the wishlist, but dedicated to working groups? I really have no idea. Just something, somewhere to centralize our goals. Regardless, thank you for the supportive voice Julien. I am glad to have your support. -- Brett M. Gilio <bre...@posteo.net> GNU Guix, Contributor <https://guix.gnu.org/>
