diff options
| author | V3n3RiX <venerix@redcorelinux.org> | 2017-11-02 21:07:25 +0000 |
|---|---|---|
| committer | V3n3RiX <venerix@redcorelinux.org> | 2017-11-02 21:07:25 +0000 |
| commit | 27dfd272ae3be15b1017f733682211afa1c7c0f0 (patch) | |
| tree | 1fe1c9ed5c5d79c63069bb8d541be075ccc3aac2 /sci-mathematics | |
| parent | d950fa39dbe16d164ed0cb8e3036fd5d0d896a4c (diff) | |
gentoo resync : 02.11.2017
Diffstat (limited to 'sci-mathematics')
3 files changed, 29 insertions, 3 deletions
diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index 226a3ac30a8b..75815e00d3f5 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -1,4 +1,4 @@ -AUX why3-for-spark-2017-gentoo.patch 488 SHA256 7fe1764ad2502c9983023417e1645299ae9a141e683f2a2b6abdf9fe5920ee7f SHA512 53c31e57021e1f7f9ca3e74447be403f99bff8009634ef400b72c48a15458230f1007e26c4070e04e3bea732d596a68ea20717a413ea13282a518d2eb29c6215 WHIRLPOOL 8514135f362dd67512a19095bfc15fcee2f22e07c9e23a069f18a7bd9e4a4ff15218a8c5368a56a6cefedc3e40ef11051a07243c315f05105c8f083145663fb1 +AUX why3-for-spark-2017-gentoo.patch 1300 SHA256 d96d6043d0c4e103ea7a35bf98daa40ef05417e94833fe6d07524a27d7af66ee SHA512 7ec992b1d0f0f285903b69876b853a8d368c73f4ed3dfccc25f5ae18e72e0c6f71ce9b81e18f2a685d19a7bfa8e69571cb71d4faa5ec67e0fbf2231202c2ea3d WHIRLPOOL 87256925a66ce0f4829fca043657c4804f0293493770904c2492174107a764a0a06ff73b87e2ded72334222cc9def467e50e45e59eea43cd9b7f2539b956dbdc DIST why3-for-spark-gpl-2017-src.tar.gz 9248235 SHA256 7e7aee3912421847c416bc1f066ac342e811601c29d7b69e98e789a59a724d8e SHA512 8f444402f6c1744cd7c565117732935791b1ae7996a94314c40a66d125eae8a81f2257314246c94fd29d3cd16abcff6a50a152a1191a4aae39a2c8a8d7c3b9e1 WHIRLPOOL 256648567b3a220f762c7e30d0f90265fd10af21b66c3607b9072e81444b0a33dc971126232e11f3edc64eac2598fbd3ad428d063f2c9db8d247be2abe5be904 -EBUILD why3-for-spark-2017.ebuild 1633 SHA256 1d3767e35c285d3933cadd73f315de72abd9433bb63e3eda874d8def4177ae0f SHA512 7ddb95b779680f509f338ecf6bbef138c99294ccc203c18e5a813e008dc0ac38dddf5c622e00f6ed2d910ab716075a8e6244922cf701fd104ccaa6c4e4b799bd WHIRLPOOL 8ea4774e4a7d113f83e8ffecfb0985ca68b230d3fbbe6d53ebd012e625bfac3e4a0a3f9e47d123556048a1ae0ac02664916aa688a1f7d47d1bfcd366502fd5ed +EBUILD why3-for-spark-2017.ebuild 1641 SHA256 47738b095e90645f913d9d55dac2272791ce3bc2a3e0cce327db90ccac71b367 SHA512 0c5940ecbb09fc3ea379ead9eec3bd6ae9ef080323dde2367c0094315425671d38c8b5bb876e7821aa35f6bc2d66535515255083a881f4c17ea020ab773f1c04 WHIRLPOOL 57e332eb27aab292001082a5fad688f7a83b2d37d5b27c1dfa4b433badd1e09dc8f17dd7cd5261fb5c826578aa3dca02587a95afa8bc2063b00e8e67e7715f83 MISC metadata.xml 1363 SHA256 013b66bd8ddb397a162291f83ed6744ea78521b89ed4014f67ad7f794aa2a3d5 SHA512 ee8323cc37fdea800e355fc14ba67cac66c3ec3c41528d481a7e938b1d3e23859bdddfb06d3b6653725cdcfcc0d07e66ba1d3cc80b3637a781db7bab5f7dc677 WHIRLPOOL f0804ec3311720be99db48f0839ee7269a4aba8ea6c07ea8abb69591c281fca7719b565694f47c43797debcafe65d19005674a1e53e13a8c9701257f50333bf8 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 502f394afa2b..225d081ca7f9 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 c143320a492d..3fd441065140 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) \ |