Dear,
Thank you for the explanations.
On Tue, 18 Feb 2020 at 12:17, Orians, Jeremiah (DTMB)
wrote:
> Finally I'll have to convince my wife to let me spend $10K to implement the
> design in hardware using: https://libresilicon.com/
> (But at least I'll have plenty of free chips to share with th
>> > The term "nothing" is mitigated; i.e. "nothing" means: a booted system
>> > running a (linux) kernel. Right?
>> No, I mean bootstrapped from bare metal.
>> No Kernel
>> No firmware
>> No microcode
>> No Bios
>> Just individual TTL logic circuits
> Is it ready yet?
Well the parts all the way t
Dear,
On Thu, 13 Feb 2020 at 13:07, Orians, Jeremiah (DTMB)
wrote:
>
> > The term "nothing" is mitigated; i.e. "nothing" means: a booted system
> > running a (linux) kernel. Right?
> No, I mean bootstrapped from bare metal.
> No Kernel
> No firmware
> No microcode
> No Bios
> Just individual TTL
> ISTR someone made an initrd with guile in it, and "booted to guile."
Yep amazing work that it is; someone also made emacs an initrd too
> If that is so, does that not suggest that "from nothing" could be independent
> of a running kernel?
Actually no, bare metal is a bit different than running
> The term "nothing" is mitigated; i.e. "nothing" means: a booted system
> running a (linux) kernel. Right?
No, I mean bootstrapped from bare metal.
No Kernel
No firmware
No microcode
No Bios
Just individual TTL logic circuits
https://github.com/oriansj/stage0
> Thank you for all your contributio
Hi Guix,
On +2020-02-12 15:16:47 +0100, zimoun wrote:
> Dear,
>
> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
> wrote:
>
> > We also have a scheme bootstrappable from nothing written in C
> > https://github.com/oriansj/mes-m2
> > https://github.com/oriansj/mescc-tools-seed
>
> The te
Svante Signell writes:
> On Wed, 2020-02-12 at 15:16 +0100, zimoun wrote:
>> Dear,
>>
>> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
>> wrote:
>>
>> > We also have a scheme bootstrappable from nothing written in C
>> > https://github.com/oriansj/mes-m2
>> > https://github.com/oriansj/
On Wed, 2020-02-12 at 15:16 +0100, zimoun wrote:
> Dear,
>
> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
> wrote:
>
> > We also have a scheme bootstrappable from nothing written in C
> > https://github.com/oriansj/mes-m2
> > https://github.com/oriansj/mescc-tools-seed
>
> The term "no
Dear,
On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
wrote:
> We also have a scheme bootstrappable from nothing written in C
> https://github.com/oriansj/mes-m2
> https://github.com/oriansj/mescc-tools-seed
The term "nothing" is mitigated; i.e. "nothing" means: a booted system
running a
> I'm interested on this topic and I will try to help as much as I can.
Good
> 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 whe
Hi all,
I know I'm a bit late to the party but I want to express my support
for this initiative.
I have very little knowledge about formal methods - extracted from
this thread, a few conversations with Brett and from skimming through
the Wikipedia page. Despite this, I find the idea of a Formal M
Hi Amin & Brett,
Amin Bandali skribis:
>> It’s fine to host the repo on Savannah: we can ask for a new repo under
>> the Guix umbrella, the downside being that access control will be the
>> same as for the other repos (we can only grant access to all the repos
>> or none of them.) If you plan t
Hello,
Ludovic Courtès writes:
> Hello!
>
> (Cc: maintainers.)
>
> Brett Gilio skribis:
>
>> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>>
>>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
>>> Also
Hi Ludo’, all,
Ludovic Courtès writes:
> Hello!
>
> (Cc: maintainers.)
>
> Brett Gilio skribis:
>
>> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>>
>>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
Hello!
(Cc: maintainers.)
Brett Gilio skribis:
> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>
>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
>> Also, is a channel developed
>> by colleagues at Inr
Dec 30, 2019 3:34:22 PM Ludovic Courtès :
> Guix-HPC is “institutional”, that’s part of the reason behind this.
> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
> Also, is a channel developed
> by colleagues at Inria, so it’s more convenient to have it there.
Hey Lud
Hello,
Brett Gilio skribis:
> Ludovic Courtès writes:
>
>> The domain name would have to be discussed with others (other
>> maintainers in particular; perhaps a better choice would be
>> formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but
>> the idea sounds great to me!
>
> Th
Vicente Eduardo writes:
Hi Vincente,
> 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.
What is "a C compiler for Scheme"? We are working on a C compiler
written in Schem
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 k
Hi Ludo’, all,
Thanks for your vote(s) of confidence, Ludo’; it’s great to hear!
Ludovic Courtès writes:
> Hi!
>
> Brett Gilio 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 s
Ludovic Courtès writes:
> For the record, I don’t work with the formal methods people at Inria,
> but we chat occasionally, and I’d be happy to draw their attention to
> this effort. :-)
I thought not, but I think this smells of potential for collaboration
maybe amongst a few there. I know some
Ludovic Courtès writes:
> The domain name would have to be discussed with others (other
> maintainers in particular; perhaps a better choice would be
> formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but
> the idea sounds great to me!
That is, of course, reasonable that we shou
Ludovic Courtès writes:
> Hi!
>
> Julien Lepiller skribis:
>
>> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
>> itself (using a bootstrapped bytecode interpreter written in C) to
>> build itself. Fortunately this situation is being worked on by a phd
>> student of Xavier
Hi Brett,
Brett Gilio skribis:
> 1. Just as the bootstrappability and guix-hpc projects have their own
> websites documenting their efforts, I think it would be nice to have
> https://fm.guix.gnu.org/ which would host a Haunt-generated
> website. This website would be hosted in the Savannah proj
Hi!
Julien Lepiller skribis:
> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
> itself (using a bootstrapped bytecode interpreter written in C) to
> build itself. Fortunately this situation is being worked on by a phd
> student of Xavier Leroy (and nixOS user) :).
>
> The
Hi!
Brett Gilio skribis:
> Having Guix and the Formal Methods community aligned would mean a great
> deal of power for both camps! Just as we see with the Software Heritage
> project and Guix, for providing historical and state-consistent
> reproducible environments for software testing we and c
Hi!
Brett Gilio 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!
> Ludo, what do you think about an https://fm.guix.gnu.org/ URL hosting a
> haun
Ludovic Courtès writes:
> Hi!
>
> Julien Lepiller skribis:
>
>> I forgot to metion I have a small channel at
>> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
>> every coq version since 8.6. I use it to test my coquille plugin on
>> every coq version that exists, but I'm sure
Hi!
Julien Lepiller skribis:
> I forgot to metion I have a small channel at
> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
> every coq version since 8.6. I use it to test my coquille plugin on
> every coq version that exists, but I'm sure there are other use cases
> :)
Tha
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA256
Amin Bandali writes:
> Hello Guix!
>
> Thank you Brett for taking initiative and putting this awesome proposal
> together on all our behalves, and to everyone else for chiming in and
> expressing your interest and support!
>
> To share some of my (
Hello Guix!
Thank you Brett for taking initiative and putting this awesome proposal
together on all our behalves, and to everyone else for chiming in and
expressing your interest and support!
To share some of my (scattered) thoughts on this, as a researcher I
think reproducible and verifiable res
John Soo writes:
> Hey this is great!
>
> I’m a hobbyist too but I’m glad to see a formal methods community in Guix!
> I’ll be following.
>
> - John
Thank you for voicing your support John! Glad to see there is an
inspiring community following for this idea.
--
Brett M. Gilio
GNU Guix, Con
Jack Hill writes:
> I'm not a formal methods researcher, but merely a hobbyist who is
> interested in programming languages and type system. That said, I find
> this proposal intriguing, and would like to follow along, and perhaps
> help as I am able. At the very least, I hope to learn some new t
Julien Lepiller writes:
> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
> itself (using a bootstrapped bytecode interpreter written in C) to
> build itself. Fortunately this situation is being worked on by a phd
> student of Xavier Leroy (and nixOS user) :).
>
> The plan i
zimoun writes:
> Hi,
>
> I am not a Programming Language Theory guy so I speak as a pure noob. :-)
> Well, I am working in University Paris 7 Diderot doing some scientific
> computing.
We are all noobs of formal methods next to Vladimir Voevodsky, and
Grothendiek. ;)
>> so this could be more of
Julien Lepiller writes:
> I forgot to metion I have a small channel at
> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
> every coq version since 8.6. I use it to test my coquille plugin on
> every coq version that exists, but I'm sure there are other use cases
> :)
>
Nice! N
Julien Lepiller 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 op
Hey this is great!
I’m a hobbyist too but I’m glad to see a formal methods community in Guix!
I’ll be following.
- John
Greetings,
On Sun, 15 Dec 2019, Brett Gilio wrote:
Hello Guix!
This is going to be a rather lengthy email proposing a new working group
(if that is indeed the proper name for this) in the GNU Guix
project. Just as there are other "working groups" for GNOME packages,
bootstrapping Rust & JVM, a
Le 16 décembre 2019 20:46:28 GMT+01:00, zimoun a
écrit :
>Hi,
>
>I am not a Programming Language Theory guy so I speak as a pure noob.
>:-)
>Well, I am working in University Paris 7 Diderot doing some scientific
>computing.
>
>
>On Mon, 16 Dec 2019 at 02:00, Brett Gilio wrote:
>
>> so this could
Hi,
I am not a Programming Language Theory guy so I speak as a pure noob. :-)
Well, I am working in University Paris 7 Diderot doing some scientific
computing.
On Mon, 16 Dec 2019 at 02:00, Brett Gilio wrote:
> so this could be more of a chance to see bigger institutions begin to
> adopt Guix
I forgot to metion I have a small channel at
https://framagit.org/tyreunom/guix-coq-channel that keeps track of every coq
version since 8.6. I use it to test my coquille plugin on every coq version
that exists, but I'm sure there are other use cases :)
Le 16 décembre 2019 01:59:59 GMT+01:00, Brett Gilio a écrit
:
>Hello Guix!
>
> ...
>
>What follows is proposals for some of the work to be done by this
>working group:
>
>-- A lot of proof assistants are based on dialects of ML. Most of these
> use SMLnj or MLton for their work. To date there i
Hello Guix!
This is going to be a rather lengthy email proposing a new working group
(if that is indeed the proper name for this) in the GNU Guix
project. Just as there are other "working groups" for GNOME packages,
bootstrapping Rust & JVM, and bootstrapping the entirely of the GNU
Corelibs (GNU
44 matches
Mail list logo
