[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Proposal] The Formal Methods in GNU Guix Working Group

From: Vicente Eduardo
Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group
Date: Sat, 28 Dec 2019 12:28:09 +0100

I'm interested on this topic and I will try to help as much as I can.

The original idea of Brett is very interesting. In my case I would do the base compiler implemented in C and using yacc (for example) to implement the grammar. But it won't make sense in a community like Guix where most people know Scheme rather than C/C++. So it may make sense to write a small C compiler for Scheme and then write the ML bootstrap compiler in Scheme, similar to what Guix does to bootstrap itself with nyacc.

This will solve more problems than Guix itself, because it seems this bootstrapping problem comes historically from the very first implementations of ML.

As we talked yesterday with Brett via chat, PolyML is the only one that has been packaged in Guix but it is very tricky, because they have on the repo the binaries to boostrap itself.

Writting a Scheme compiler should be easy, if we don't care about optimization techniques. It doesn't need that requirements. But if you need any help in the low level area, I can help you guys.


El sáb., 28 dic. 2019 8:21, Amin Bandali <address@hidden> escribió:
Hi Ludo’, all,

Thanks for your vote(s) of confidence, Ludo’; it’s great to hear!

Ludovic Courtès <address@hidden> writes:

> Hi!
> Brett Gilio <address@hidden> skribis:
>> 100% Agreed. Amin is also working on packaging the Lean prover and I am
>> taking an interest in seeing if we can extend the OPAM importer to have
>> a subimporter for Coq.
> That’d be nice!

I just sent in the very first patch inspired (in part) by this proposal
to guix-patches: :-)

>> Ludo, what do you think about an URL hosting a
>> haunt webpage designed by Amin and I (and maybe others) to detail the
>> purpose, goal, and maybe institutional use cases (research papers) of
>> GNU Guix in the formal methods community?
> The domain name would have to be discussed with others (other
> maintainers in particular; perhaps a better choice would be
> or, next to, but
> the idea sounds great to me!

Sure!  I’d love to hear from others (esp. other maintainers) about this.

Personally, being a GNU maintainer, webmaster, and Savannah hacker, I’m
(almost by definition :-)) partial to using * and various pieces
of the GNU infra (lists, Savannah source repositories, …) for GNU work
whenever possible.  As such, I naturally like better as
the domain, and would prefer to use Savannah for hosting our sources,
e.g. the Haunt sources for the Guix-FM site.

What do you think?

Like Brett, I’d be curious to hear the reasons for using * and
a non-Savannah repository forge for Guix-HPC.

> Thanks,
> Ludo’.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]