From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 ) for ; 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 ) for ; 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 ; 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 ) 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 ) 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 ) 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 ) 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" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 29 Jun 2020 07:11:02 +0000 Resent-Message-ID: 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 Cc: Jakub =?UTF-8?Q?K=C4=85dzio=C5=82ka?= , 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 ) 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 ) 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: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" Reply-to: elaexuotee@wilsonb.com, elaexuotee--- via Guix-patches From: elaexuotee--- via Guix-patches via 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_=_--