Re: bug#38529: Make --ad-hoc the default for guix environment proposed deprecation mechanism

[Konrad Hinsen]

On 16/12/2019 23:09, Ludovic Courtès wrote:

So in a more algorithmic manner:

1. if ad-hoc and inputs-of is present at the same invocation: fail
hard. (With an error like incompatible options present)
2. if only ad-hoc is present, then print a deprecation warning (yes,
we could make this suspendable with an environment variable, like you
described)
3. if only inputs-of present, then do the new behaviour.
4. if neither ad-hoc nor inputs-of present then
   a. if GUIX_ENVIRONMENT_DEPRECATED is 1: do the current behaviour,
   b. if GUIX_ENVIRONMENT_DEPRECATED is undefined, or is not 1: do the
new behaviour.

That sounds like a good plan to me.

#4 is the trickiest, and I think it’d be good to give users a bit of
time so they can start adjusting before deprecation is in effect.


#4 is trickiest for another reason: there is no future-proof use of 
"guix environment" that works right now and will continue to work. Nor 
is there any way to see, when looking at a command line, whether it's 
old-style or new-style, if neither --ad-hoc nor --inputs-of are present. 
This means that all existing documentation (tutorials etc.) will become 
misleading in the future. Worse, even documentation written today, in 
full awareness of a coming change, can't do better than saying "watch 
out, this will do something else in the future".


The first rule of backwards-compatibility is: never change the meaning 
of an existing valid command/API. Add new valid syntax, deprecate old 
valid syntax, but don't change the meaning of something that was and 
will be valid.


How about a more drastic measure: deprecate "guix environment" and 
introduce a new subcommand with the desired new behaviour?



Cheers,

  Konrad.

Importers as independent packages?

[Martin Becze]

Hello Guix,
I have been working on a recursive importer that uses semantic
versioning over on #38408. It relies on guile-semver. I'm not exactly
sure how to add guile-semver as a dependency to guix. But I'm also not
sure that I should. Importers will probably not be used by the majority
of end users so would it make sense to put the importers in their own
package? This would also nicely solve recursive-import-semver's problem
of being dependent on guile-semver. 

Also in the future it would be nice if the crate import could read from
a Cargo.toml directly (this will make importing things like alacritty
much easier since it is not crates.io), which would probably mean have
yet another dependency (guile-toml). What do you think about this Guix?

Thanks,
-Martin Becze

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

[Brett Gilio]

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, Contributor 

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

[Brett Gilio]

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

I am glad you say this. We all have a lot to learn from each other here.

> One of the things that attracted me to Guix is the ability to
> represent the pieces as objects in a programming language as opposed
> the the big mass of state that is a traditional system. I agree this
> property of Guix harmonizes with formal analysis.

Absolutely! This is the kind of thesis I was proposing, and something
that I wonder what Julien will think of as far as benefits particular
and specific to the formal methods community.

>> 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 is an issue of
>>   source-based bootstrapping of _all_ of the major ML compilers. We do
>>   have PolyML in our repositories, but even this uses space-inefficient
>>   text file blobs for compiling and is not a fully C-based source
>>   bootstrap. Basically, all of the ML compilers rely on some distinct
>>   pre-compiled something-or-other to get to their pristine state. I
>>   have explored the idea, along with Leo and Amin, about following in
>>   the tradition of MES (and mrustc) and starting an analogous GNU project for
>>   writing a reduced-size specification ML bootstrapping compiler. That
>>   way we can end the loop of a source-based build of ML97 compilers
>>   being basically impossible.
>>   [See issues #38605 & #38606 on DEBBUGS. Also, see
>>   https://github.com/MLton/mlton/issues/350.]
>
> This is the sub-area I'm most interested in. In addition to ML, I'd
> also like to be able to bootstrap GHC. I know that Ricardo has done
> some work in that area [0].
>
> [0]
> https://elephly.net/posts/2017-01-09-bootstrapping-haskell-part-1.html

So far this idea has garnered the most attention. Amin Bandali and I are
both wanting to see this be taken to the next level, with maybe the
support of Janneke and other people working with minimal compilers /
formal methods in their day-to-day work. See some of my previous emails
to others about why I think this is important work. Basically, as I
mentioned to Ludo' the situation of bootstrapping ML from source is
occluded after 1993. We should reasonably be able to remedy this in
order to facilitate ML-based proof assistant development and use on
Guix. Especially things like the PRLs (NuPRL, RedPRL, JonPRL) which
offer nice dependent type systems. But first the compiler tower needs to
be there."

Maybe we could borrow some inspiration from miniML (mentioned by
Julien), CakeML (mentioned by Simon), or C Minor? I don't know. But I
think this is an important task.

> Thanks for proposing the idea!
>
> All the best,
> Jack

Thank you for voicing your support Jack! :)

-- 
Brett M. Gilio 
GNU Guix, Contributor 

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

[Brett Gilio]

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 is to write a compiler in C or Scheme (it currently exists,
> but is written in OCaml) for "miniML" a small subset of the OCaml
> language. Then, there is already an interpreter in miniML able to
> interpret the OCaml compiler compiling itself. Once the miniML
> compiler is bootstrapped, we will have a path from C to OCaml :)

I did not know of this project. Thank you for telling me!

-- 
Brett M. Gilio 
GNU Guix, Contributor 

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

[Brett Gilio]

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 a chance to see bigger institutions begin to
>> adopt Guix for their research work.
>
> IMHO, today the "win" is not about bootstrapping because it is
> strongly language dependent but this "win" offered by Guix is about
> the time-traveling reproducibility tools: today the key point in
> scientific research (IMHO).
> And yes, the reproducibility over the time means bootstrappability.
> But it is each scientific community that must take care of its
> outputs.
>
> The wider adoption could come from features as "time-machine",
> available packages (channels for the not GNU compliant), easy to
> distribute, to reproduce, be able to search in all the packages over
> all the Guix history, etc.

Undoubtedly the formal methods community, just as with all other
communities of scientific research stands to benefit from the
time-machine! No question about that. I would be intrigued to see in
what ways we can push that paradigm to its limits. Formal methods is
notorious for finding novel ways to bring change to our systems of
abstraction, and challenge our notions of things like "safety". So maybe
the time-machine could still stand to benefit from improvement, and maybe the 
formal
methods community by using it will find out ways to do that. Purely
speculation, here.

>> -- A lot of proof assistants are based on dialects of ML. Most of these
>>use SMLnj or MLton for their work. To date there is an issue of
>>source-based bootstrapping of _all_ of the major ML compilers. We do
>>have PolyML in our repositories, but even this uses space-inefficient
>>text file blobs for compiling and is not a fully C-based source
>>bootstrap. Basically, all of the ML compilers rely on some distinct
>>pre-compiled something-or-other to get to their pristine state. I
>>have explored the idea, along with Leo and Amin, about following in
>>the tradition of MES (and mrustc) and starting an analogous GNU project 
>> for
>>writing a reduced-size specification ML bootstrapping compiler. That
>>way we can end the loop of a source-based build of ML97 compilers
>>being basically impossible.
>>[See issues #38605 & #38606 on DEBBUGS. Also, see
>>https://github.com/MLton/mlton/issues/350.]
>
> It is a ambitious research project. Woow! Nice!! :-)
>
> CakeML [1] claims to be a subset of Standard ML and to be
> boostrappable. I do not know enough to have an relevant opinion.
>
> [1] https://cakeml.org/

I am quite familiar with CakeML, and I draw a lot of inspiration with
the things they are managing to do as a subset implementation of ML. I
think it would be interesting to see where a bootstrapping compiler
could go if it were fledged out into a full implementation for the GNU
project, filling a dual-role. Again, just proposing some ideas. :)

> What is the status of OCaml about boostrappability?

Julien answered this already, but there is a gap here.

> Yes, let spread the world! :-)
>
> And IMO a good start is to show in scientific communities why
> boostrappability matters.
>
> For example, the papers which were OK in [2] (2015), are they still OK
> in 2019? I bet that a lot of big binary blobs have disappear since
> then.
>
> [2] http://repeatability.cs.arizona.edu/
>
>
>
> All the best,
> simon

Simon, I am glad to have your support here! Please engage with us more
as more details come. You may be a "noob" (self-reported), but it is
noobs who provide us the most valuable information often times.

-- 
Brett M. Gilio 
GNU Guix, Contributor 

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

[Brett Gilio]

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 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 
GNU Guix, Contributor 

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

[John Soo]

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

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

[Jack Hill]

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, and bootstrapping the entirely of the GNU
Corelibs (GNU Mes) in Guix, I am proposing a new working group based on
the synthesis of two fundamentally and mutually agreeable concepts.

This is a continuation of the discussion proposed by Amin Bandali, Leo
Prikler, and I from the #guix Freenode IRC. All three of us are either
students of formal methods in mathematics and computer science, users of
proof assistants, or interested in category theory and type theory. As
such as noticed and wondered what kind of community there is for formal
methods in GNU Guix, and by extension what kind of benefits GNU Guix has
to offer the formal methods community which is providing some of the
most rigorous research in computing methods to date.


[…]


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 correspond to
formal methods much of the same guarantees of deterministic
computational states, modeling, and reasoning in software correctness.


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


One of the things that attracted me to Guix is the ability to represent 
the pieces as objects in a programming language as opposed the the big 
mass of state that is a traditional system. I agree this property of Guix 
harmonizes with formal analysis.


[…]


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 is an issue of
  source-based bootstrapping of _all_ of the major ML compilers. We do
  have PolyML in our repositories, but even this uses space-inefficient
  text file blobs for compiling and is not a fully C-based source
  bootstrap. Basically, all of the ML compilers rely on some distinct
  pre-compiled something-or-other to get to their pristine state. I
  have explored the idea, along with Leo and Amin, about following in
  the tradition of MES (and mrustc) and starting an analogous GNU project for
  writing a reduced-size specification ML bootstrapping compiler. That
  way we can end the loop of a source-based build of ML97 compilers
  being basically impossible.
  [See issues #38605 & #38606 on DEBBUGS. Also, see
  https://github.com/MLton/mlton/issues/350.]


This is the sub-area I'm most interested in. In addition to ML, I'd also 
like to be able to bootstrap GHC. I know that Ricardo has done some work 
in that area [0].


[0] https://elephly.net/posts/2017-01-09-bootstrapping-haskell-part-1.html


-- Begin adding more projects that are important works in the formal
  methods community. We have Coq, Idris, and Agda, but there is a lot of work
  to be done on keeping these projects not only up-to-date but also
  adding subprojects that use these toolchains. For example: C Minor,
  Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
  RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
  various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
  Haskell, extensions to Z3, and tons more!


I would love to have more tools like these in Guix, so that we can use 
Guix's repoducibility guarantees to have them as part of the historical 
record.



All of this seems really nice and impressive, but what is it without
getting some feedback from the community? I'd _really_ love to hear your
thoughts, experiences, and more on this working group idea and other
working groups to avoid pitfalls. Maybe we should have a secondary
#guix-fm channel on IRC? There is definitely a lot of work to be done
here, and we will need some form of organizational structure to keep the
work consistent and neatly integrated with the goals and purposes of GNU
Guix.

I hope to hear from the community.


Thanks for proposing the idea!

All the best,
Jack

Re: TeX Live 2019 wanted

[Marius Bakke]

Marius Bakke  writes:

> Andreas Enge  writes:
>
>> I gave it a try, dropped the patches, then the phase use-code-for-new-poppler
>> fails for texlive-bin; maybe these poppler phases can be dropped, but I am
>> not quite familiar with them.
>
> The 'use-code-for-new-poppler' phase needs to be rewritten along these
> lines (for both 2018 and 2019):

Errh, the patch only works if you already have Poppler 0.83.0.  For the
current 'core-updates' branch, I believe you can use the same approach
but fetch poppler-0.76.0.cc instead (or take Arch's patch[0]).

[0] 
https://git.archlinux.org/svntogit/packages.git/tree/trunk?h=packages/texlive-bin


signature.asc
Description: PGP signature

Re: TeX Live 2019 wanted

[Ricardo Wurmus]

Marius Bakke  writes:

> Wrt the other TeX packages, I think %texlive-tag and %texlive-revision
> from (guix build-system texlive) needs to be bumped, and all the hashes
> changed accordingly.

Yes, that’s pretty much it.  It’s a little tedious as so many hashes
will be invalidated at once.

There may also be a few instances where the list of files to be included
in the “SVN source union” will have to be adjusted, but I hope that this
is no longer a common issue since the last time I tried to more closely
match the outputs of our packages with the upstream file lists.

--
Ricardo

Re: bug#38529: Make --ad-hoc the default for guix environment proposed deprecation mechanism

[Ludovic Courtès]

Hello,

Gábor Boskovits  skribis:

> So in a more algorithmic manner:
> 1. if ad-hoc and inputs-of is present at the same invocation: fail
> hard. (With an error like incompatible options present)
> 2. if only ad-hoc is present, then print a deprecation warning (yes,
> we could make this suspendable with an environment variable, like you
> described)
> 3. if only inputs-of present, then do the new behaviour.
> 4. if neither ad-hoc nor inputs-of present then
>   a. if GUIX_ENVIRONMENT_DEPRECATED is 1: do the current behaviour,
>   b. if GUIX_ENVIRONMENT_DEPRECATED is undefined, or is not 1: do the
> new behaviour.

That sounds like a good plan to me.

#4 is the trickiest, and I think it’d be good to give users a bit of
time so they can start adjusting before deprecation is in effect.

Namely, we could start by introducing ‘--inputs-of’ and emitting a
warning in case #4 to suggest the use of ‘--inputs-of’.  Apart from the
warning, case #4 would still behave the same as now.

Three (?) months later, we implement what you describe above.  Hopefully
by that time many people got used to ‘--inputs-of’.

Thoughts?

Ludo’.

Re: When to add rust packages?

[John Soo]

Hi all,

I submitted my patches this morning in #38640.  Thanks for the continued work 
on the rust build system.  I like rust tools quite a lot.

- John

Re: Report from the 2019 Reproducible Builds Summit

[Pjotr Prins]

On Mon, Dec 16, 2019 at 03:33:24PM +0100, Pierre Neidhardt wrote:
> As usual I've learned a lot from this great read!

Indeed. I am also very interested in the time machine :). Try and do
that with Ansible.

Pj.

Re: TeX Live 2019 wanted

[Marius Bakke]

Andreas Enge  writes:

> I gave it a try, dropped the patches, then the phase use-code-for-new-poppler
> fails for texlive-bin; maybe these poppler phases can be dropped, but I am
> not quite familiar with them.

The 'use-code-for-new-poppler' phase needs to be rewritten along these
lines (for both 2018 and 2019):

diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm
index d184d7616b..9184bd1552 100644
--- a/gnu/packages/tex.scm
+++ b/gnu/packages/tex.scm
@@ -238,6 +238,15 @@ copied to their outputs; otherwise the TEXLIVE-BUILD-SYSTEM is used."
 (sha256 (base32
  "1b8zigzg8raxkhhzphcmynf84rbdbj2ym2qkz24v8n0qx82zmqms"
 
+(define (texlive-svn-file name revision hash)
+  (origin
+(method url-fetch)
+(uri (string-append "https://tug.org/svn/texlive/trunk/Build/source/;
+name "?revision=" revision "=co"))
+(file-name (string-append "texlive-" (match (string-split name #\/)
+   ((dirs ... file-name) file-name
+(sha256 (base32 hash
+
 (define-public texlive-bin
   (package
(name "texlive-bin")
@@ -285,6 +294,12 @@ copied to their outputs; otherwise the TEXLIVE-BUILD-SYSTEM is used."
   (sha256
(base32
 "0wrjls1y9b4k1z10l9l8w2l3yjcw7v7by2y16kchdpkiyldlkry6"
+  ("pdftosrc-poppler-compat"
+   ,(texlive-svn-file "texk/web2c/pdftexdir/pdftosrc-poppler0.83.0.cc" "52959"
+  "0iq2cmwvf2lxy32sygrafwqgcwvvbdnvxm5l3mrg9cb2a1g06380"))
+  ("pdftoepdf-poppler-compat"
+   ,(texlive-svn-file "texk/web2c/pdftexdir/pdftoepdf-poppler0.83.0.cc" "52959"
+  "0981acbsig4pqbhg3a2ghiygd0zv1kqvmncacigfzvpj5r5k8px1"))
   ("cairo" ,cairo)
   ("fontconfig" ,fontconfig)
   ("fontforge" ,fontforge)
@@ -356,10 +371,10 @@ copied to their outputs; otherwise the TEXLIVE-BUILD-SYSTEM is used."
(string-append "\"" (assoc-ref inputs "ghostscript") "/bin/gs\"")))
 #t))
 (add-after 'unpack 'use-code-for-new-poppler
-  (lambda _
-(copy-file "texk/web2c/pdftexdir/pdftoepdf-poppler0.76.0.cc"
+  (lambda* (#:key inputs #:allow-other-keys)
+(copy-file (assoc-ref inputs "pdftoepdf-poppler-compat")
"texk/web2c/pdftexdir/pdftoepdf.cc")
-(copy-file "texk/web2c/pdftexdir/pdftosrc-poppler0.76.0.cc"
+(copy-file (assoc-ref inputs "pdftosrc-poppler-compat")
"texk/web2c/pdftexdir/pdftosrc.cc")
 #t))
 (add-after 'use-code-for-new-poppler 'use-code-for-even-newer-poppler

Can you try that?

Wrt the other TeX packages, I think %texlive-tag and %texlive-revision
from (guix build-system texlive) needs to be bumped, and all the hashes
changed accordingly.

Thanks!


signature.asc
Description: PGP signature

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

[Julien Lepiller]

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 be more of a chance to see bigger institutions begin to
>> adopt Guix for their research work.
>
>IMHO, today the "win" is not about bootstrapping because it is
>strongly language dependent but this "win" offered by Guix is about
>the time-traveling reproducibility tools: today the key point in
>scientific research (IMHO).
>And yes, the reproducibility over the time means bootstrappability.
>But it is each scientific community that must take care of its
>outputs.
>
>The wider adoption could come from features as "time-machine",
>available packages (channels for the not GNU compliant), easy to
>distribute, to reproduce, be able to search in all the packages over
>all the Guix history, etc.
>
>And what I see as a blocking wider adoption by the Researcher around
>me is: Mac. A lot of them just use Mac, I mean they develop daily on
>MacOS and then once it is ready run on linux HPC clusters.
>
>I know the article by Ludo and Ricardo. :-) And I strongly agree.
>From my point of view, the only way to attract more researchers is to
>have an half-baked Guix working on Mac, IMHO.
>
>
>> -- A lot of proof assistants are based on dialects of ML. Most of
>these
>>use SMLnj or MLton for their work. To date there is an issue of
>>source-based bootstrapping of _all_ of the major ML compilers. We
>do
>>have PolyML in our repositories, but even this uses
>space-inefficient
>>text file blobs for compiling and is not a fully C-based source
>>bootstrap. Basically, all of the ML compilers rely on some
>distinct
>>pre-compiled something-or-other to get to their pristine state. I
>>have explored the idea, along with Leo and Amin, about following
>in
>>the tradition of MES (and mrustc) and starting an analogous GNU
>project for
>>writing a reduced-size specification ML bootstrapping compiler.
>That
>>way we can end the loop of a source-based build of ML97 compilers
>>being basically impossible.
>>[See issues #38605 & #38606 on DEBBUGS. Also, see
>>https://github.com/MLton/mlton/issues/350.]
>
>It is a ambitious research project. Woow! Nice!! :-)
>
>CakeML [1] claims to be a subset of Standard ML and to be
>boostrappable. I do not know enough to have an relevant opinion.
>
>[1] https://cakeml.org/
>
>What is the status of OCaml about boostrappability?

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 is to write a compiler in C or Scheme (it currently exists, but is 
written in OCaml) for "miniML" a small subset of the OCaml language. Then, 
there is already an interpreter in miniML able to interpret the OCaml compiler 
compiling itself. Once the miniML compiler is bootstrapped, we will have a path 
from C to OCaml :)

>
>
>> -- Begin giving talks on the benefits of GNU Guix at conferences
>around
>>Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.
>
>Yes, let spread the world! :-)
>
>And IMO a good start is to show in scientific communities why
>boostrappability matters.
>
>For example, the papers which were OK in [2] (2015), are they still OK
>in 2019? I bet that a lot of big binary blobs have disappear since
>then.
>
>[2] http://repeatability.cs.arizona.edu/
>
>
>
>All the best,
>simon

Re: Remarks about commit 2c82d4ad10de8

[Brett Gilio]

Brett Gilio  writes:

> I think you are correct. I likely made a mistake. We should revert the change.
>
> Thanks!
>
> Dec 16, 2019 9:13:31 AM Mathieu Othacehe :
>
>> 
>> Hello Brett,
>> 
>> I have a few remarks on the aforementioned commit.
>> 
>> 
>> > + (list (string-append "-DCMAKE_CXX_FLAGS='-isystem "
>> > + (assoc-ref %build-inputs "gcc")
>> > + "/include/c++'"
>> > 
>> 
>> Why is this needed? The following snippet in clang-from-llvm isn't enough?
>> 
>> --8<---cut here---start->8---
>> ;; Make clang look for libstdc++ in the right
>> ;; location.
>> (("LibStdCXXIncludePathCandidates\\[\\] = \\{")
>> (string-append
>> "LibStdCXXIncludePathCandidates[] = { \"" gcc "/include/c++\","))
>> --8<---cut here---end--->8---
>> 
>> 
>> > + (inputs
>> > `(("clang" ,clang)
>> > - ("llvm" ,llvm)))
>> > + ("ncurses" ,ncurses)))
>> > + (native-inputs
>> > + `(("rapidjson" ,rapidjson)
>> > 
>> 
>> Rapidjson is an input (even if ccls is not linked against because its a
>> header-only library).
>> 
>> 
>> > + ("gcc" ,gcc)))
>> > 
>> 
>> This shouldn't be needed as it is an implicit input.
>> 
>> Thanks,
>> 
>> Mathieu
>> 
>
>

Mathieu,

I have reverted the affected commits. Thank you for bringing the issue
to my attention.

-- 
Brett M. Gilio
GNU Guix, Contributor 

Re: TeX Live 2019 wanted

[Andreas Enge]

I gave it a try, dropped the patches, then the phase use-code-for-new-poppler
fails for texlive-bin; maybe these poppler phases can be dropped, but I am
not quite familiar with them.

Andreas

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

[zimoun]

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 for their research work.

IMHO, today the "win" is not about bootstrapping because it is
strongly language dependent but this "win" offered by Guix is about
the time-traveling reproducibility tools: today the key point in
scientific research (IMHO).
And yes, the reproducibility over the time means bootstrappability.
But it is each scientific community that must take care of its
outputs.

The wider adoption could come from features as "time-machine",
available packages (channels for the not GNU compliant), easy to
distribute, to reproduce, be able to search in all the packages over
all the Guix history, etc.

And what I see as a blocking wider adoption by the Researcher around
me is: Mac. A lot of them just use Mac, I mean they develop daily on
MacOS and then once it is ready run on linux HPC clusters.

I know the article by Ludo and Ricardo. :-) And I strongly agree.
>From my point of view, the only way to attract more researchers is to
have an half-baked Guix working on Mac, IMHO.


> -- A lot of proof assistants are based on dialects of ML. Most of these
>use SMLnj or MLton for their work. To date there is an issue of
>source-based bootstrapping of _all_ of the major ML compilers. We do
>have PolyML in our repositories, but even this uses space-inefficient
>text file blobs for compiling and is not a fully C-based source
>bootstrap. Basically, all of the ML compilers rely on some distinct
>pre-compiled something-or-other to get to their pristine state. I
>have explored the idea, along with Leo and Amin, about following in
>the tradition of MES (and mrustc) and starting an analogous GNU project for
>writing a reduced-size specification ML bootstrapping compiler. That
>way we can end the loop of a source-based build of ML97 compilers
>being basically impossible.
>[See issues #38605 & #38606 on DEBBUGS. Also, see
>https://github.com/MLton/mlton/issues/350.]

It is a ambitious research project. Woow! Nice!! :-)

CakeML [1] claims to be a subset of Standard ML and to be
boostrappable. I do not know enough to have an relevant opinion.

[1] https://cakeml.org/

What is the status of OCaml about boostrappability?


> -- Begin giving talks on the benefits of GNU Guix at conferences around
>Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

Yes, let spread the world! :-)

And IMO a good start is to show in scientific communities why
boostrappability matters.

For example, the papers which were OK in [2] (2015), are they still OK
in 2019? I bet that a lot of big binary blobs have disappear since
then.

[2] http://repeatability.cs.arizona.edu/



All the best,
simon

Presentations for the Guix Days! (FOSDEM 2020)

[Pjotr Prins]

As Andreas pointed out, the Guix days are an unconference. That is, it
gets organized on the spot so we have ample time to discuss important
topics and hack.

Even so, we would like to invite a few short presentations (15
minutes) for the two mornings. We are not looking for introductory
talks, but it may be good to prepare and bring up material that can be
used the rest of the day (and is of general interest). I, for one,
would not mind to hear a talk on hacking Guix in the REPL ;)

After the talk(s) we'll have a plenary to discuss Guix progress,
where we want to go and what we want to achieve while being in
Brussels (i.e., what working groups to form). This should only last
half an hour. The rest of the day is for resolving outstanding issues
and generating fruitful collaborations. 

So, if anyone has a good idea for a talk feel free to post to Manolis,
Ludo and/or me.

Pj.

PS I forgot to mention last time, but it is possible to stay at the
ICAB venue. It is basic but cheap and Guix talk starts early at
breakfast. Just E-mail the folks at http://www.icab.be/

On Tue, Dec 10, 2019 at 06:43:51AM -0600, Pjotr Prins wrote:
> Dear all,
> 
> FOSDEM is coming early February and not only are we organizing the GNU
> Guix days, we also have a devroom with exciting talks on Guile, Guix,
> and Mes! See 
> 
>   https://libreplanet.org/wiki/Group:Guix/FOSDEM2020
> 
> and
> 
>   
> https://fosdem.org/2020/schedule/track/minimalistic_experimental_and_emerging_languages/
> 
> FOSDEM is the greatest free software conference on earth (in my opinion)
> and almost everyone who goes once keeps coming because there is
> something for everyone. 
> 
> See last years amazing program for Saturday:
> 
>   https://archive.fosdem.org/2019/schedule/day/saturday/
> 
> Both FOSDEM and Guix days are free to attend! The evening program is
> great too - you can find hacker nirvana.
> 
> We can only receive up to 40 people for the Guix days (last year we
> had 35) and we need to reserve the catering. So, please sign up on the
> libreplanet link above, if you intend to come. If we happen to have
> too many people to attend the meeting the 40 who signed up have a
> guaranteed entry. If you don't want to subscribe to the wiki you can
> send us a request to add.
> 
> Pjotr & Manolis.
> 
>  n Fri, Feb 22, 2019 at 05:20:41PM +0100, Ricardo Wurmus wrote:
> > Hi Guix,
> > 
> > Chris Marusich kindly took the time to write a detailed report about a
> > session from the Guix Days, and it’s now up on the Guix blog:
> > 
> > https://www.gnu.org/software/guix/blog/2019/guix-days-bootstrapping-arm/
> > 
> > I don’t want to spoil it for you, so I encourage you to take a peek at
> > it yourselves to read about challenges of the past, the present, and the
> > future when it comes to bootstrapping ARM systems.
> > 
> > Not only does the blog post explain the problems and technical fixes,
> > but Chris takes a few steps back to look at the bigger picture and
> > invites you to think big.
> > 
> > Enjoy!
> > 
> > --
> > Ricardo
> > 
> > 
> 

Re: The Guix Days: stream?

[Pjotr Prins]

On Sun, Dec 15, 2019 at 02:51:20AM +0100, zimoun wrote:
> Hi Andreas,
> 
> 
> > First question: do we want?
> 
> Pjotr: yes
> Andreas: no
> 
> That's why I raised the question. :-)
> 
> 
> In summary:
>  - it seems complicated to stream in live because of the ICAB network.
>  - we could still record chunks and upload them a bit later.
> 
> Other opinions / answers to the question: do we want to record?

Certainly. At least the talks. More on that in the next mail.

Pj.

Re: TeX Live 2019 wanted

[Andreas Enge]

Hello,

On Sat, Dec 14, 2019 at 08:06:19PM +0100, Marius Bakke wrote:
> Ricardo, do you think you'll have time for a TeX Live 2019 update in the
> coming weeks?  If not, could you outline the required changes for
> enterprising Guix contributors?

before your mail I had already tried to update the monolithic texlive, but
one of the patches did not apply any more; since I did not know what they
were for, I pushed it to the back of the queue. From what you write, I
suppose the patches could simply be dropped?

Then I was unsure how updating the texlive sources would impact the
modular texlive packages. Is anything special needed?

Andreas

Re: The Guix Days: stream?

[zimoun]

Hi Andreas,


> First question: do we want?

Pjotr: yes
Andreas: no

That's why I raised the question. :-)


In summary:
 - it seems complicated to stream in live because of the ICAB network.
 - we could still record chunks and upload them a bit later.

Other opinions / answers to the question: do we want to record?


All the best,
simon

Re: The Guix Days: stream?

[Andreas Enge]

On Thu, Dec 12, 2019 at 06:57:27PM +0100, zimoun wrote:
> Previously, we discussed on the possibility to video stream chunks of
> these 2 days.

Honestly, I do not think it is a good idea for an "un-conference".
These two days are more devoted to hacking, hands-on activities and
spontaneous working groups, and less for "formal" talks; the latter have
their place in the FOSDEM track.

Andreas

Re: Remarks about commit 2c82d4ad10de8

[Brett Gilio]

I think you are correct. I likely made a mistake. We should revert the change.

Thanks!

Dec 16, 2019 9:13:31 AM Mathieu Othacehe :

> 
> Hello Brett,
> 
> I have a few remarks on the aforementioned commit.
> 
> 
> > + (list (string-append "-DCMAKE_CXX_FLAGS='-isystem "
> > + (assoc-ref %build-inputs "gcc")
> > + "/include/c++'"
> > 
> 
> Why is this needed? The following snippet in clang-from-llvm isn't enough?
> 
> --8<---cut here---start->8---
> ;; Make clang look for libstdc++ in the right
> ;; location.
> (("LibStdCXXIncludePathCandidates\\[\\] = \\{")
> (string-append
> "LibStdCXXIncludePathCandidates[] = { \"" gcc "/include/c++\","))
> --8<---cut here---end--->8---
> 
> 
> > + (inputs
> > `(("clang" ,clang)
> > - ("llvm" ,llvm)))
> > + ("ncurses" ,ncurses)))
> > + (native-inputs
> > + `(("rapidjson" ,rapidjson)
> > 
> 
> Rapidjson is an input (even if ccls is not linked against because its a
> header-only library).
> 
> 
> > + ("gcc" ,gcc)))
> > 
> 
> This shouldn't be needed as it is an implicit input.
> 
> Thanks,
> 
> Mathieu
> 

Re: qtwenengine anybody?

[Hartmut Goebel]

Am 16.12.19 um 18:09 schrieb mike.ros...@gmail.com:
> I'm currently brushing up my latest qtwebengine build. Will resubmit
> this patch. I will also see if I can inherit qtsvg again to put this
> back on par with other module packages. From there I'll put a simple
> test example together demonstrating the locale and translation problem.

Sounds good

-- 
Regards
Hartmut Goebel

| Hartmut Goebel  | h.goe...@crazy-compilers.com   |
| www.crazy-compilers.com | compilers which you thought are impossible |

Re: guix pull broke: Unbound variable: substitute-keyword-arguments

[Pierre Neidhardt]

You mean for the offending commit?

-- 
Pierre Neidhardt
https://ambrevar.xyz/


signature.asc
Description: PGP signature

Re: qtwenengine anybody?

[Hartmut Goebel]

Am 16.12.19 um 16:45 schrieb mike.ros...@gmail.com:
> The problem is also not readily obvious until you
> try to use qtwebengine in a library or a program. Which will causes
> locale and translation path issues.

If the only issue with qtwebengine are locale and translation, I suggest
to accept these for now. IMHO we need to attract more users (and
developers) for guix, fir which we need more packages.  And missing
qtwebengine blocks some KDE applications form getting build for guix.

-- 
Regards
Hartmut Goebel

| Hartmut Goebel  | h.goe...@crazy-compilers.com   |
| www.crazy-compilers.com | compilers which you thought are impossible |

Re: qtwenengine anybody?

[mike . rosset]

Hartmut Goebel  writes:

> Hi,
>
> I'm glad to see there already has been some effort on this. I'll comment
> on the issue.
>
> Am 16.12.19 um 15:13 schrieb mike.ros...@gmail.com:
>> This new monolithic package stills suffers from the same issue as my
>> modular qtwebengine. In that there are many in tree third party
>> dependencies. It's not trivial to simply switch to guix inputs for
>> these.
>
> IMO we should focus on a stand-alone qtwebengine package to avoid having
> packages depending on a *huge* monolith.

This is the most ideal situation. However the modular qtwebengine makes
some assumptions which are not compatible with guix. For examples it
assumes it will be installed in the same prefix as qtbase. Which is not
possible with guix. The problem is also not readily obvious until you
try to use qtwebengine in a library or a program. Which will causes
locale and translation path issues.

For the nomad browser I had had some hacks to get around this. But those
hacks won't work in all cases. Because it's dependent on arg0
location. Which is not consistent when using an interpreter like guile
or python or if you are using qtwebengine from a dynamic library.
As of yet I have not found a proper way to resolve this.

I believe the monolithic qt package at this time is the shortest route
to having a sane working qtwebengine, until the locale issues can be
resolved.

Mike

Re: guix pull broke: Unbound variable: substitute-keyword-arguments

[Ricardo Wurmus]

Pierre Neidhardt  writes:

> It works now, however it does not detect the breakage introduced by the
> aforementioned commit.

“guix pull” also worked for me.

-- 
Ricardo

Re: qtwenengine anybody?

[Hartmut Goebel]

Hi,

I'm glad to see there already has been some effort on this. I'll comment
on the issue.

Am 16.12.19 um 15:13 schrieb mike.ros...@gmail.com:
> This new monolithic package stills suffers from the same issue as my
> modular qtwebengine. In that there are many in tree third party
> dependencies. It's not trivial to simply switch to guix inputs for
> these.

IMO we should focus on a stand-alone qtwebengine package to avoid having
packages depending on a *huge* monolith.


-- 
Regards
Hartmut Goebel

| Hartmut Goebel  | h.goe...@crazy-compilers.com   |
| www.crazy-compilers.com | compilers which you thought are impossible |

Re: qtwenengine anybody?

[mike . rosset]

Pierre Neidhardt  writes:

> Mike, can you give some details (maybe one example) on how to replace the
> third-party dependencies?  What is holding it back?
>
> I could give it a go if need be.

I have not tackled this problem yet. I've mainly been focused on get the
package to build. I've fixed the most blaring issue. For example the
package now builds in parallel which improves build times significantly.

In terms of resolving the in tree dependencies. Some can be resolved
using QT configure flags. I don't think I've ported these over from my
module qtwebengine but I will check this when I have time.

The other third party dependencies might need header and gn
substitutions. A good place to start is the ugoogled-chromium package as
to how this is done. Though it might take more work for qtwebengine
because of QT configure and build changes. That's about as far as I got
with looking at this.

Mike

Remarks about commit 2c82d4ad10de8

[Mathieu Othacehe]

Hello Brett,

I have a few remarks on the aforementioned commit.

> +   (list (string-append "-DCMAKE_CXX_FLAGS='-isystem "
> +(assoc-ref %build-inputs "gcc")
> +"/include/c++'"

Why is this needed? The following snippet in clang-from-llvm isn't enough?

--8<---cut here---start->8---
;; Make clang look for libstdc++ in the right
;; location.
(("LibStdCXXIncludePathCandidates\\[\\] = \\{")
 (string-append
  "LibStdCXXIncludePathCandidates[] = { \"" gcc "/include/c++\","))
--8<---cut here---end--->8---

> + (inputs
>   `(("clang" ,clang)
> -   ("llvm" ,llvm)))
> +   ("ncurses" ,ncurses)))
> +(native-inputs
> + `(("rapidjson" ,rapidjson)

Rapidjson is an input (even if ccls is not linked against because its a
header-only library).

> +   ("gcc" ,gcc)))

This shouldn't be needed as it is an implicit input.

Thanks,

Mathieu

Re: Report from the 2019 Reproducible Builds Summit

[Pierre Neidhardt]

As usual I've learned a lot from this great read!

Out of curiosity, why is "janneke" spelled without a capital? :)

-- 
Pierre Neidhardt
https://ambrevar.xyz/


signature.asc
Description: PGP signature

Package runtime dependencies (see bug#38576)

[Lars-Dominik Braun]

Hi,

in light of bug#38576 I filed, I’d like to get some guidance on when to pull in
dependencies. The package in question is r-irkernel, which is essentially an R
package bridging between Jupyter and R. However, it would never be “imported”
by the user like other R packages. Instead Jupyter executes R and tells it to
run an IPC server written in R. Thus I would consider r-minimal a runtime
dependency of r-irkernel. (If r-minimal is not installed then R_LIBS_SITE is
not set and R can’t find the package IRkernel whenever Jupyter tries to run R
code.)

python-ipykernel however does *not* explicitcy depend on python, even though it
works exactly the same, whereas jupyter-guile-kernel depends on guile.

Any thoughts on this?

Thanks,
Lars

Re: qtwenengine anybody?

[mike . rosset]

Pierre Neidhardt  writes:

> Mike Rosset had it working in a patch that's still waiting on the tracker.
> It has at least one issue as far as I get it.  Mike also made an
> all-in-one "Qt" package that does not suffer from this issue, a bit like
> our texlive mega-package.
>
> I'm all for adding it to master.

Thanks for forwarding this to me Pierre. The new monolithic QT packages
with qtwebengine is derived from the now deprecated qt package, which
has since been removed from guix, which is understandable since the
module packages are more ideal.

This new monolithic package stills suffers from the same issue as my
modular qtwebengine. In that there are many in tree third party
dependencies. It's not trivial to simply switch to guix inputs for
these.

This package is an improvement on my module qtwebengine package. Since
it does not suffer from the same locales issues.

Mike

Re: qtwenengine anybody?

[Pierre Neidhardt]

Mike, can you give some details (maybe one example) on how to replace the
third-party dependencies?  What is holding it back?

I could give it a go if need be.

-- 
Pierre Neidhardt
https://ambrevar.xyz/


signature.asc
Description: PGP signature

Report from the 2019 Reproducible Builds Summit

[Ludovic Courtès]

Hello Guix!

Some of us were lucky enough to be in Marrakesh a couple of weeks ago
for the Reproducible Builds Summit.  You can read about some of what we
discussed and hacked on here:

  https://guix.gnu.org/blog/2019/reproducible-builds-summit-5th-edition/

Feedback welcome!

Ludo’.


signature.asc
Description: PGP signature

Re: qtwenengine anybody?

[Pierre Neidhardt]

Mike Rosset had it working in a patch that's still waiting on the tracker.
It has at least one issue as far as I get it.  Mike also made an
all-in-one "Qt" package that does not suffer from this issue, a bit like
our texlive mega-package.

I'm all for adding it to master.

-- 
Pierre Neidhardt
https://ambrevar.xyz/


signature.asc
Description: PGP signature

Re: guix pull broke: Unbound variable: substitute-keyword-arguments

[Pierre Neidhardt]

It works now, however it does not detect the breakage introduced by the
aforementioned commit.

-- 
Pierre Neidhardt
https://ambrevar.xyz/


signature.asc
Description: PGP signature

qtwenengine anybody?

[Hartmut Goebel]

Hi Guix!

Looks like we need to package qtwebengine, as more and more packages
require it.
qtwebengine includes a copy of chromium.

Any volunteers?

-- 
Regards
Hartmut Goebel

| Hartmut Goebel  | h.goe...@crazy-compilers.com   |
| www.crazy-compilers.com | compilers which you thought are impossible |

Ansible and GuixOps questions

[rchar01]

Hello,

Probably many admins / DevOps are heavily using Ansible. I also use this 
solution to configure systems and services (on Debian and CentOS).
I would like to transfer infrastructure to the Guix System and some questions 
arose:

- is there any way to combine Ansible and GuixOps?
- is there any way to continue using Ansible to configure Guix (some in guile 
script and some in ansible)?
- would it be possible to generate a guile script (for GuixOps) from Ansible?
- would it be possible to change the Ansible to talk to the Guix (or GuixOps) 
system?

Rewriting to Guile (Guix config files):
* Against:
** time consuming
** may require new skills
** only for Guix, Ansible can configure other GNU / Linux systems
* What might the benefits be?

Such integration would probably help to transfer from other systems to Guix and 
enlarge the community.
What do you think?

Regards,
Robert.

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

[Julien Lepiller]

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

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

[Julien Lepiller]

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 is an issue of
>   source-based bootstrapping of _all_ of the major ML compilers. We do
>  have PolyML in our repositories, but even this uses space-inefficient
>   text file blobs for compiling and is not a fully C-based source
>   bootstrap. Basically, all of the ML compilers rely on some distinct
>   pre-compiled something-or-other to get to their pristine state. I
>   have explored the idea, along with Leo and Amin, about following in
>the tradition of MES (and mrustc) and starting an analogous GNU project
>for
>   writing a reduced-size specification ML bootstrapping compiler. That
>   way we can end the loop of a source-based build of ML97 compilers
>   being basically impossible.
>   [See issues #38605 & #38606 on DEBBUGS. Also, see
>   https://github.com/MLton/mlton/issues/350.]
>
>-- Begin adding more projects that are important works in the formal
>methods community. We have Coq, Idris, and Agda, but there is a lot of
>work
>   to be done on keeping these projects not only up-to-date but also
>   adding subprojects that use these toolchains. For example: C Minor,
>   Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
>   RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
>   various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
>   Haskell, extensions to Z3, and tons more!

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.

>-- Possibly begin formally verifying some of the behavior and
>   implementations of GNU Guix and GNU Guile. This is kind of an add-on
>   idea, but it struck our interest so why leave it out?
>
>-- Begin giving talks on the benefits of GNU Guix at conferences around
>   Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

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?

>All of this seems really nice and impressive, but what is it without
>getting some feedback from the community? I'd _really_ love to hear
>your
>thoughts, experiences, and more on this working group idea and other
>working groups to avoid pitfalls. Maybe we should have a secondary
>#guix-fm channel on IRC? There is definitely a lot of work to be done
>here, and we will need some form of organizational structure to keep
>the
>work consistent and neatly integrated with the goals and purposes of
>GNU
>Guix.

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.

>I hope to hear from the community.
>
>Thanks,