From mboxrd@z Thu Jan 1 00:00:00 1970 From: Amin Bandali Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Fri, 03 Jan 2020 18:49:13 -0500 Message-ID: <87eewg5cee.fsf@gnu.org> References: <87tv616q5s.fsf@posteo.net> <141B1FAE-6518-4E0C-8E69-C96BCB540545@lepiller.eu> <878smxegxp.fsf@gnu.org> <87tv5ls8kj.fsf@gnu.org> <871rspe3x3.fsf@gnu.org> <875zi1qhoc.fsf@gnu.org> <87o8vp1os4.fsf@gnu.org> <87blrlse36.fsf@gnu.org> Mime-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:37041) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1inWgv-0003ih-1N for guix-devel@gnu.org; Fri, 03 Jan 2020 18:49:18 -0500 In-Reply-To: <87blrlse36.fsf@gnu.org> List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: Ludovic =?utf-8?Q?Court=C3=A8s?= Cc: guix-devel@gnu.org, GNU Guix maintainers --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hi Ludo=E2=80=99, all, Ludovic Court=C3=A8s writes: > Hello! > > (Cc: maintainers.) > > Brett Gilio skribis: > >> Dec 30, 2019 3:34:22 PM Ludovic Court=C3=A8s : >> >>> Guix-HPC is =E2=80=9Cinstitutional=E2=80=9D, that=E2=80=99s part of the= reason behind this. >>> Regarding gitlab.inria.fr, that=E2=80=99s because it used to be hosted = at Inria. >>> Also, is a channel developed >>> by colleagues at Inria, so it=E2=80=99s more convenient to have it ther= e. >> >> >> Hey Ludo, thanks for the explanation. >> >> It makes sense why Guix-HPC lives somewhere else. Given this, what >> do you propose for initiating the conversation on where the formal >> methods haunt page should live with the other maintainers? I >> personally think the repository should live on Savannah, but the >> address needs to be discussed. > > It=E2=80=99s 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 to open it more to formal methods people > that do not yet contribute to Guix, it might be easier to use a separate > repo. You tell us! > Right. Thinking about this, as I see it right now I think our use cases for repos fall roughly into two categories: =2D Closely Guix-related or small standalone things: this could be things like the Haunt sources for our site, or a Guix channel for additional package definitions, or anything closely related to Guix and/or small enough to fit under the Guix umbrella just fine. For these, we should be able to get by with a very small number of repos in the short and long term. Initially, we will only have one such repository, say, guix/guix-fm.git or guix/formal-methods.git, with its purpose being mainly to keep the sources for the site. For these repos we=E2=80=99ll happily accept patches from folks who aren= =E2=80=99t Guix contributors via mailing list. And I=E2=80=99d imagine once they ha= ve contributed enough patches, we could work out getting them commit access, especially if their gathered knowledge/experience extends to Guix directly (e.g. in form of familiarity with package definitions and writing them). =2D Larger projects or ones that don=E2=80=99t quite fit the scope of Guix:= for these, we might indeed consider registering separate Savannah projects rather than putting them under the Guix project. I think the proposed bootstrapping ML compiler could be an example of such project. All that said, I do wish Savannah supported finer access control at the project level. I just asked a fellow Savannah hacker for his opinion on whether implementing that would be possible and feasible with the current underlying infrastructure in mind. > > As for the domain name: I think it would be fine to use > formal-methods.guix.gnu.org as long as the web site follows GNU and Guix > policy, which mostly means referring only to free software, avoiding the > phrase =E2=80=9Copen source=E2=80=9D to describe it, and probably avoidin= g institution > logos and such (I don=E2=80=99t think there=E2=80=99s any written policy = but I would > personally find it out of place on gnu.org.) Anyway, the two of you are > webmasters so you probably know this better than I do. IOW, if you want > to flatter your employers and labs, you might want to opt for a separate > web site. :-) > Most certainly; I wouldn=E2=80=99t expect anything less. :-) As for institution logos, agreed. If it ever comes such time that we absolutely =E2=80=9Chave to=E2=80=9D consider that, I=E2=80=99ll be sure to= check with you and the other Guix maintainers, fellow GNU webmasters, and of course rms. As for the domain name, I think formal-methods.guix.gnu.org is a bit of a mouthful to type or say on a regular basis, and I think an abbreviated fm.guix.gnu.org would be more convenient; =C3=A0 la ci.guix.gnu.org. For what it=E2=80=99s worth, I=E2=80=99ve seen the FM abbreviation for Formal M= ethods used fairly commonly around the community. Lastly, I think it would be nice to have a guix-fm@gnu.org address for Guix-FM. Rather than a full-fledged Mailman list, I think a simple alias, like with guix-hpc@gnu.org, will suffice. Thoughts? > > Maintainers, what do you think? > > Anyway, step #1 is to get a web page ready. :-) > > Ludo=E2=80=99. I=E2=80=99ll work on putting one together over the next couple of days. :-) Best, amin --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQJEBAEBCAAuFiEEObM8jZRIDS3cwqSYi0Sgzce5VvIFAl4P0vkQHGJhbmRhbGlA Z251Lm9yZwAKCRCLRKDNx7lW8kvpEACSQgau4JKaAkXk7UAgGVw87cQA4VyUCRHv huAMxsGREdoGMFvVaqqbU++MQWyQ+v7Leh4RpfRfxDSVeSRy4L/cpaCicDnnwaDE oGlSz4UqWIUskIrC3ywq165Xxo+HNnO5e3QDZ6aru45uDyFWKdj2Bzj/mYTwZ/v5 xClJmT7TPE3jJCdJzapHC6l8W4T190rU/l9h5Fs8mR2J6WZXJyzhNip/eeeRMxva rowONcnQievyqSmjRyXz3Kta9Gy9WVx6Prt5orq5smE79Aka2G+Vv4O1oyRk+8QR CPnZfgTVPfZkqlXjyzlvalbR+C/3jZAU6uiHeABKtQPb1MISWl6uLMKRgLmGB4Ey m0pFZ0y6aE3UtNmncoQxHGe4gJve/vjJ9HGGhPjMV60ES3ovtHKI4lBgV4UmkRqt spCkiRhXoyT5bPy/2+wnmh9axDsDb2cVxHR6UWb65REIWeYEsqZD46URezTOxOwh nGc7yS6ZF+Yfos3EOh5NT5yL0rxR+6ChmlhofyHCpLN+707SqVO6OyfMwuNiTK+X MxqdVbUlDEdwIQEMMT2VWfapx06l/ZfQnKLe2FLclD1HMpj07C2hmoDcufK2Jnz7 CXMRtUeZLUpCdo0m+BXl68eZg5CfrnNz6HJFIyP2qSiBgGcKpAZKPSSL70krcFKK Lw1kXtz9vw== =5g2t -----END PGP SIGNATURE----- --=-=-=--