From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([209.51.188.92]:48513) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gqlfu-0002zb-CU for guix-patches@gnu.org; Mon, 04 Feb 2019 16:21:07 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gqlfq-0003It-QG for guix-patches@gnu.org; Mon, 04 Feb 2019 16:21:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:60480) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gqlfq-0003IP-Io for guix-patches@gnu.org; Mon, 04 Feb 2019 16:21:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gqlfq-0000BJ-5r for guix-patches@gnu.org; Mon, 04 Feb 2019 16:21:02 -0500 Subject: [bug#34299] [PATCH] gnu: Add coq-autosubst Resent-Message-ID: Received: from eggs.gnu.org ([209.51.188.92]:48215) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gqlex-0002FG-3y for guix-patches@gnu.org; Mon, 04 Feb 2019 16:20:08 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gqlew-00027H-4R for guix-patches@gnu.org; Mon, 04 Feb 2019 16:20:07 -0500 Received: from lepiller.eu ([89.234.186.109]:45834) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gqlev-00024u-Qc for guix-patches@gnu.org; Mon, 04 Feb 2019 16:20:06 -0500 Received: from localhost (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id fb23279e (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 4 Feb 2019 21:19:59 +0000 (UTC) Date: Mon, 4 Feb 2019 22:19:56 +0100 From: Julien Lepiller Message-ID: <20190204221956.33848890@lepiller.eu> In-Reply-To: <20190203152426.5750-1-dfrumin@cs.ru.nl> References: <20190203152426.5750-1-dfrumin@cs.ru.nl> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 34299@debbugs.gnu.org Hi Dan, thanks for the patch! Some notes below: Le Sun, 3 Feb 2019 16:24:26 +0100, Dan Frumin a =C3=A9crit : > --- > gnu/packages/coq.scm | 45 > ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 > insertions(+) >=20 > diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm > index 51dd5dedc..ba1bfd93b 100644 > --- a/gnu/packages/coq.scm > +++ b/gnu/packages/coq.scm > @@ -444,3 +444,48 @@ provides BigN, BigZ, BigQ that used to be part > of Coq standard library.") simplifying the proofs of inequalities on > expressions of real numbers for the Coq proof assistant.") > (license license:cecill-c))) > + > +(define-public coq-autosubst > + (let ((branch "coq86-devel") > + (commit "d0d73557979796b3d4be7aac72135581c33f26f7")) So, why this commit and this branch in particular? It seems that there are some releases on github, and we tend to prefer using a released version of packages. > + (package > + (name "coq-autosubst") > + (synopsis "A Coq library for parallel de Bruijn substitutions") > + (version (git-version "1" branch commit)) > + (source (origin > + (method git-fetch) > + (uri (git-reference > + (url "git://github.com/uds-psl/autosubst.git") > + ;; (branch branch) Please remove these comments :) > + (commit commit))) > + (file-name (git-file-name name version)) > + (sha256 > + (base32 > "1852xb5cwkjw3dlc0lp2sakwa40bjzw37qmwz4bn3vqazg1hnh6r")))) > + (build-system gnu-build-system) > + (native-inputs > + `(("coq" ,coq))) > + (arguments > + `(#:tests? #f > + #:phases > + (modify-phases %standard-phases > + (delete 'configure) > + (replace 'install > + (lambda* (#:key outputs #:allow-other-keys) > + (setenv "COQLIB" (string-append (assoc-ref outputs > "out") "/lib/coq/")) > + (zero? (system* "make" > + (string-append "COQLIB=3D" (assoc-ref > outputs "out") > + "/lib/coq/") > + "install"))))))) We now use (invoke ...) instead of (zero? (system* ...)). > + (description "Formalizing syntactic theories with variable > binders is +not easy. We present Autosubst, a library for the Coq > proof assistant to +automate this process. Given an inductive > definition of syntactic objects in +de Bruijn representation > augmented with binding annotations, Autosubst +synthesizes the > parallel substitution operation and automatically proves the +basic > lemmas about substitutions. Our core contribution is an automation > +tactic that solves equations involving terms and substitutions. This > makes the +usage of substitution lemmas unnecessary. The tactic is > based on our current +work on a decision procedure for the equational > theory of an extension of the +sigma-calculus by Abadi et. al. The > library is completely written in Coq and +uses Ltac to synthesize the > substitution operation.") > + (home-page "https://www.ps.uni-saarland.de/autosubst/") > + (license bsd-3)))) Thank you!