From: ludo@gnu.org (Ludovic Courtès)
To: Julien Lepiller <julien@lepiller.eu>
Cc: 27444@debbugs.gnu.org
Subject: [bug#27444] coq libraries
Date: Thu, 22 Jun 2017 21:39:09 +0200 [thread overview]
Message-ID: <87mv8zrew2.fsf@gnu.org> (raw)
In-Reply-To: <20170621214539.756fd583@lepiller.eu> (Julien Lepiller's message of "Wed, 21 Jun 2017 21:45:39 +0200")
Hi Julien,
Julien Lepiller <julien@lepiller.eu> skribis:
> From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Thu, 8 Jun 2017 18:25:32 +0200
> Subject: [PATCH 1/5] gnu: Add coq-flocq.
>
> * gnu/packages/ocaml.scm (coq-flocq): New variable.
LGTM.
> + `(#:configure-flags
> + (list (string-append "--libdir=" (assoc-ref %outputs "out")
> + "/lib/coq/user-contrib/Flocq"))
Should we add a search path specification in Coq for “lib/coq”?
> From 2aa65616e6b478fb539e6a9a8bf00285e054e7f4 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Wed, 21 Jun 2017 21:38:42 +0200
> Subject: [PATCH 2/5] gnu: Add coq-gappa.
>
> * gnu/packages/ocaml.scm (coq-gappa): New variable.
[...]
> + (home-page "http://gappa.gforge.inria.fr/")
> + (synopsis "Verify and formally prove properties on numerical programs")
> + (description "Gappa is a tool intended to help verifying and formally proving
> +properties on numerical programs dealing with floating-point or fixed-point
> +arithmetic. It has been used to write robust floating-point filters for CGAL
> +and it is used to certify elementary functions in CRlibm. While Gappa is
> +intended to be used directly, it can also act as a backend prover for the Why3
> +software verification plateform or as an automatic tactic for the Coq proof
> +assistant.")
> + (license (list license:gpl2 license:cecill))))
Please indicate if it’s a mixture of both licenses or a choice up to the
user. Also, double-check whether it’s ‘gpl2’ and not ‘gpl2+’.
Otherwise LGTM.
> From 67fd96b375b25c83f4be5be82ce963ad1a3f651e Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Wed, 21 Jun 2017 21:39:33 +0200
> Subject: [PATCH 3/5] gnu: Add coq-mathcomp.
>
> * gnu/packages/ocaml.scm (coq-mathcomp): New variable.
LGTM.
> From 2ef53eb922f64b4f359704ef06a796339efc776f Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Wed, 21 Jun 2017 21:40:23 +0200
> Subject: [PATCH 4/5] gnu: Add coq-coquelicot.
>
> * gnu/packages/ocaml.scm (coq-coquelicot): New variable.
LGTM.
> From a76224a176850d38ae2bc80a6d77493ab3fffa41 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Wed, 21 Jun 2017 21:41:36 +0200
> Subject: [PATCH 5/5] gnu: Add coq-interval.
>
> * gnu/packages/ocaml.scm (coq-interval): New variable.
OK!
Thank you,
Ludo’.
next prev parent reply other threads:[~2017-06-22 19:40 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-06-21 19:45 [bug#27444] coq libraries Julien Lepiller
2017-06-22 19:39 ` Ludovic Courtès [this message]
2017-07-27 18:44 ` Julien Lepiller
2017-07-28 19:48 ` Ludovic Courtès
2017-07-30 8:55 ` bug#27444: " Julien Lepiller
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87mv8zrew2.fsf@gnu.org \
--to=ludo@gnu.org \
--cc=27444@debbugs.gnu.org \
--cc=julien@lepiller.eu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.