From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 7B3C71396D9 for ; Wed, 1 Nov 2017 20:31:57 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 8E33DE0EB1; Wed, 1 Nov 2017 20:31:56 +0000 (UTC) Received: from smtp.gentoo.org (smtp.gentoo.org [IPv6:2001:470:ea4a:1:5054:ff:fec7:86e4]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 6CA8CE0EB1 for ; Wed, 1 Nov 2017 20:31:56 +0000 (UTC) Received: from oystercatcher.gentoo.org (oystercatcher.gentoo.org [148.251.78.52]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id 72B0F33BF01 for ; Wed, 1 Nov 2017 20:31:55 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id 1B6759188 for ; Wed, 1 Nov 2017 20:31:54 +0000 (UTC) From: "Alfredo Tupone" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Alfredo Tupone" Message-ID: <1509568229.f7767454e6ac2a9eb63c5fc48e3fe8d1fe0ff1dd.tupone@gentoo> Subject: [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/ X-VCS-Repository: repo/gentoo X-VCS-Files: sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild X-VCS-Directories: sci-mathematics/why3-for-spark/files/ sci-mathematics/why3-for-spark/ X-VCS-Committer: tupone X-VCS-Committer-Name: Alfredo Tupone X-VCS-Revision: f7767454e6ac2a9eb63c5fc48e3fe8d1fe0ff1dd X-VCS-Branch: master Date: Wed, 1 Nov 2017 20:31:54 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org X-Archives-Salt: d0be5bc0-b1d9-40a4-ae4a-a6c6d51a91a3 X-Archives-Hash: becd9c03784fdb37ce51d669916a3cdd commit: f7767454e6ac2a9eb63c5fc48e3fe8d1fe0ff1dd Author: Tupone Alfredo gentoo org> AuthorDate: Wed Nov 1 20:28:03 2017 +0000 Commit: Alfredo Tupone gentoo org> CommitDate: Wed Nov 1 20:30:29 2017 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f7767454 sci-mathematics/why3-for-spark: Enable coq tactics Package-Manager: Portage-2.3.8, Repoman-2.3.3 .../files/why3-for-spark-2017-gentoo.patch | 26 ++++++++++++++++++++++ .../why3-for-spark/why3-for-spark-2017.ebuild | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch index 502f394afa2..225d081ca7f 100644 --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch @@ -12,3 +12,29 @@ let rec file_concat l = match l with +--- why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4.old 2017-10-26 22:25:55.289094778 +0200 ++++ why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4 2017-10-26 22:26:10.719807270 +0200 +@@ -1352,7 +1352,7 @@ + let limit = + { Call_provers.empty_limit with Call_provers.limit_time = timelimit } in + let call = Driver.prove_task ~command ~limit drv !task in +- wait_on_call call ++ wait_on_call (ServerCall call) + with + | NotFO -> + if debug then Printexc.print_backtrace stderr; flush stderr; +@@ -1399,14 +1399,8 @@ + | StepLimitExceeded -> error "Step Limit Exceeded" + | HighFailure -> error ("Prover failure\n" ^ res.pr_output ^ "\n") + +-IFDEF COQ84 THEN +- +-ELSE +- + let why3tac ?timelimit s = Proofview.V82.tactic (why3tac ?timelimit s) + +-END +- + end + + TACTIC EXTEND Why3 diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild index c143320a492..3fd44106514 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild @@ -46,10 +46,10 @@ src_prepare() { src_configure() { econf \ - --disable-coq-tactic \ --disable-pvs-libs \ --disable-isabelle-libs \ $(use_enable coq coq-libs) \ + $(use_enable coq coq-tactic) \ $(use_enable doc) \ $(use_enable emacs emacs-compilation) \ $(use_enable gtk ide) \