From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <guix-patches-bounces+larch=yhetil.org@gnu.org>
Received: from mp1 ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by ms11 with LMTPS
	id OOn6Bg+U+V7qJAAA0tVLHw
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Mon, 29 Jun 2020 07:11:11 +0000
Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits))
	by mp1 with LMTPS
	id MNe0Ag+U+V58ZgAAbx9fmQ
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	for <larch@yhetil.org>; Mon, 29 Jun 2020 07:11:11 +0000
Received: from lists.gnu.org (lists.gnu.org [209.51.188.17])
	(using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits))
	(No client certificate requested)
	by aspmx1.migadu.com (Postfix) with ESMTPS id 87EA89403C9
	for <larch@yhetil.org>; Mon, 29 Jun 2020 07:11:10 +0000 (UTC)
Received: from localhost ([::1]:35318 helo=lists1p.gnu.org)
	by lists.gnu.org with esmtp (Exim 4.90_1)
	(envelope-from <guix-patches-bounces+larch=yhetil.org@gnu.org>)
	id 1jpnwa-00051c-KE
	for larch@yhetil.org; Mon, 29 Jun 2020 03:11:08 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:60980)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1jpnwU-00051S-NS
 for guix-patches@gnu.org; Mon, 29 Jun 2020 03:11:02 -0400
Received: from debbugs.gnu.org ([209.51.188.43]:36051)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <Debian-debbugs@debbugs.gnu.org>)
 id 1jpnwU-0000Ni-EW
 for guix-patches@gnu.org; Mon, 29 Jun 2020 03:11:02 -0400
Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2)
 (envelope-from <Debian-debbugs@debbugs.gnu.org>) id 1jpnwU-0004Sr-8O
 for guix-patches@gnu.org; Mon, 29 Jun 2020 03:11:02 -0400
X-Loop: help-debbugs@gnu.org
Subject: [bug#40815] gnu: Add metamath
Resent-From: elaexuotee@wilsonb.com
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces@debbugs.gnu.org>
Resent-CC: guix-patches@gnu.org
Resent-Date: Mon, 29 Jun 2020 07:11:02 +0000
Resent-Message-ID: <handler.40815.B40815.159341461417086@debbugs.gnu.org>
Resent-Sender: help-debbugs@gnu.org
X-GNU-PR-Message: followup 40815
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: 
To: Nicolas Goaziou <mail@nicolasgoaziou.fr>
Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= <kuba@kadziolka.net>,
 40815@debbugs.gnu.org
Received: via spool by 40815-submit@debbugs.gnu.org id=B40815.159341461417086
 (code B ref 40815); Mon, 29 Jun 2020 07:11:02 +0000
Received: (at 40815) by debbugs.gnu.org; 29 Jun 2020 07:10:14 +0000
Received: from localhost ([127.0.0.1]:47597 helo=debbugs.gnu.org)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <debbugs-submit-bounces@debbugs.gnu.org>)
 id 1jpnvh-0004RW-LT
 for submit@debbugs.gnu.org; Mon, 29 Jun 2020 03:10:14 -0400
Received: from m42-5.mailgun.net ([69.72.42.5]:59617)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <bounce+ca63a8.08547a-40815=debbugs.gnu.org@mg.wilsonb.com>)
 id 1jpnve-0004RB-Q6
 for 40815@debbugs.gnu.org; Mon, 29 Jun 2020 03:10:11 -0400
DKIM-Signature: a=rsa-sha256; v=1; c=relaxed/relaxed; d=mg.wilsonb.com;
 q=dns/txt; 
 s=krs; t=1593414611; h=Content-Type: MIME-Version: Message-Id:
 In-Reply-To: References: Subject: From: Cc: To: Date: Sender;
 bh=Fzwwx9370ga1BRrn9FP9NPi3099epSCfT63ZFkRl5nk=;
 b=HHy6a2vVCLoCC+yLM9jNLfCL15AX0PbRqbfH/Zkp6SjtdRwrt+kVZ0Nomz5L7qfDR4ajI7Td
 APVIGmFW1H6RSIUjbANbw71x+suKtaKzhZtQauC8ui9rJzYoHhnfa+pejg5WTwOJrNRVgSw6
 2HUoBjY5w3uHTlq/WqYvfqAMJA2y67GBGZwP5kMFAl4K3ficEpDIjTXi3Pm3Kg0T0jSZ19P3
 +UHPFZRjrNcZEBDnMHW2qsTtyl/r2JUFHj97FIe/fMHvtY7neDwMPWdAm3+kDAECGLxopajm
 VlNKptInOYf5RPq8zvJg9/4ES8E0HQ7GZUDG9gnFIM05zkC+1aaCZw==
X-Mailgun-Sending-Ip: 69.72.42.5
X-Mailgun-Sid: WyIxOGZjZiIsICI0MDgxNUBkZWJidWdzLmdudS5vcmciLCAiMDg1NDdhIl0=
Received: from wilsonb.com (wilsonb.com [104.199.203.42]) by
 smtp-out-n12.prod.us-west-2.postgun.com with SMTP id
 5ef993cc6f2ee827da274a4c (version=TLS1.3, cipher=TLS_AES_128_GCM_SHA256);
 Mon, 29 Jun 2020 07:10:04 GMT
Received: from localhost (KD111239210180.au-net.ne.jp [111.239.210.180])
 by wilsonb.com (Postfix) with ESMTPSA id 52981A1A42;
 Mon, 29 Jun 2020 07:10:01 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wilsonb.com;
 s=201703; t=1593414601;
 bh=Fzwwx9370ga1BRrn9FP9NPi3099epSCfT63ZFkRl5nk=;
 h=Date:To:Cc:From:Subject:References:In-Reply-To:From;
 b=Tx0ax26grr8QPZtzknog0auvC31eWufM5UOloExJPrMqLNZ6w5LVKYKXVrvg26JKD
 7iSEzMphnc2m4/GoesCIBPiIU1WbMjF67yqu0Uc7hMbnruCbUTGbjT1UURuvqt8mSL
 0y/jgWO1vdHo95GiDo406PhYSl6omDGy5HHroSXLVVe391rWXdtrPl+ZR20XBHhUwZ
 4vlOxym66VdZMX7HPN+UMgDst59UMPwtxCCh2GessrUNjoJ7V+yDLK9GpTURYt5VWq
 fFpyOc4j0uCPhjw/u1o9OWMnWiFSUATsC6PqybS8F6vY8xt2lbIh+8pwg3X6qc6DD2
 dkmYYi0Zqwf7weWUdFB7f/wzg+FVoyGu9KfXbDGpor2FZ9Xhz1F3NAGYYVynalKDbf
 vppKRf2CeQY+kQEsz9K27VHMM8EijX9WtH00ySL+umb4VJJtcn1pMWyfE7bN2CZS3x
 srW6+l7j6Y/E3RF7sYVVGch+n16weSQxZo0Ck3K1Sw7skwAP0RVKWmw4AhFqwR3vpv
 VFWDkrDXUjoKsTW5x85QBthHgdGuYMvw8DbyeHjBdcQLKP06BpF+18GOkylqVgJL5p
 yt5KyI+g1Egas6cV9alcvwd4+fZSN/g/EO2cnIzKkbAekK9k1iqALSkJrp10W3n73G
 U8ZUBra9FbQuLJr+rVgwa7g4=
Date: Mon, 29 Jun 2020 16:09:57 +0900
References: <3JR2ES0G0DYM2.3NI13ZSG185CK@wilsonb.com>
 <20200426172945.7ez6i2fl3pjcoexd@gravity>
 <2RKLUI9248WBS.24Y0W3OIHXG53@wilsonb.com>
 <20200427121248.cga7p43flnusf7zo@gravity>
 <3S4EBJJJJ806M.2BHUR2A6GTXWM@wilsonb.com>
 <25O95D5CM0PJ7.2ZDVSAI1CMLJL@wilsonb.com> <87d06eraaf.fsf@nicolasgoaziou.fr>
 <23UB7VNWCB6BC.23I1T2MHNG4ZI@wilsonb.com> <878sgas38j.fsf@nicolasgoaziou.fr>
 <2Z19F0HU7SZNL.33AMEA6BFHCFT@wilsonb.com> <87k0zrvtk6.fsf@nicolasgoaziou.fr>
In-Reply-To: <87k0zrvtk6.fsf@nicolasgoaziou.fr>
Message-Id: <3DWRMY6FLHG65.2WHMN0WRGUE63@wilsonb.com>
User-Agent: mblaze/0.7
MIME-Version: 1.0
Content-Type: multipart/signed; micalg="pgp-sha1";
 protocol="application/pgp-signature";
 boundary="----_=_325dd5287a9b06e46e7bf2ef_=_"
X-Spam-Score: -0.0 (/)
X-BeenThere: debbugs-submit@debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
X-Spam-Score: -1.0 (-)
X-BeenThere: guix-patches@gnu.org
List-Id: <guix-patches.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=unsubscribe>
List-Archive: <https://lists.gnu.org/archive/html/guix-patches>
List-Post: <mailto:guix-patches@gnu.org>
List-Help: <mailto:guix-patches-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/guix-patches>,
 <mailto:guix-patches-request@gnu.org?subject=subscribe>
Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org
Sender: "Guix-patches" <guix-patches-bounces+larch=yhetil.org@gnu.org>
Reply-to: elaexuotee@wilsonb.com, elaexuotee--- via Guix-patches <guix-patches@gnu.org>
From: elaexuotee--- via Guix-patches via <guix-patches@gnu.org>
X-Scanner: scn0
Authentication-Results: aspmx1.migadu.com;
	dkim=fail (rsa verify failed) header.d=mg.wilsonb.com header.s=krs header.b=HHy6a2vV;
	dkim=fail (rsa verify failed) header.d=wilsonb.com header.s=201703 header.b=Tx0ax26g;
	dmarc=none;
	spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org
X-Spam-Score: -2.11
X-TUID: aHojXJ6fMw05

This is a multipart message in MIME format.

------_=_325dd5287a9b06e46e7bf2ef_=_
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="----_=_38043db35e3d96bb4ac8a7c2_=_"

This is a multipart message in MIME format.

------_=_38043db35e3d96bb4ac8a7c2_=_
Content-Type: text/plain; charset=UTF-8
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

Hell,

Thanks for the quick turnaround.

> The book looks like a related project to metamath, like advanced
> documentation, not like a regular manual. I didn't read it, so it is
> just a guess.

Oh, okay. That makes sense. PDF as official documentation is certainly stra=
nge
for what looks like a cli program. In this case, it just happens that this =
is
the only reasonable documentation, aparth from the website, for using and
understanding Metamath proofs.

> I do. In any case, if you want to keep them, they need to start with two
> semicolons, not a single one.
>=20
> WDYT?

I trust your initial impression on this one. Let's use the patch from my
previous email that excises the commented out code. Does it look reasonable=
?

Cheers.

------_=_38043db35e3d96bb4ac8a7c2_=_--

------_=_325dd5287a9b06e46e7bf2ef_=_
Content-Disposition: attachment; filename=signature.asc
Content-Type: application/pgp-signature
Content-Transfer-Encoding: 7bit

-----BEGIN PGP SIGNATURE-----

iI0EABYIADUWIQQ7FdZn/PDWvxE6cmR2pStZ7i7CgQUCXvmTwBccZWxhZXh1b3Rl
ZUB3aWxzb25iLmNvbQAKCRB2pStZ7i7CgXEYAP98w7kcM4QTASjmbGISdN+/VghL
eva/Llu66KJVKut1ewD+KmNMLZtaoRTvkMVVy1wzmEhWvamDOsiNsC0YN8DrFQk=
=RjJ1
-----END PGP SIGNATURE-----

------_=_325dd5287a9b06e46e7bf2ef_=_--