-
Notifications
You must be signed in to change notification settings - Fork 49
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #426 from MSoegtropIMC/package-update-8.19
Package update 8.19
- Loading branch information
Showing
4 changed files
with
133 additions
and
15 deletions.
There are no files selected for viewing
25 changes: 25 additions & 0 deletions
25
...o/coq-itauto.8.19.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| From 828e973c631eeb4875ca94fb1a4d1bfb7ebc7866 Mon Sep 17 00:00:00 2001 | ||
| From: Michael Soegtrop <[email protected]> | ||
| Date: Fri, 24 Nov 2023 17:57:28 +0100 | ||
| Subject: [PATCH] Remove --root on dune calls - does not work on Windows MinGW | ||
| cygwin cross | ||
|
|
||
| --- | ||
| src/patch/Makefile | 4 ++-- | ||
| 1 file changed, 2 insertions(+), 2 deletions(-) | ||
|
|
||
| diff --git a/src/patch/Makefile b/src/patch/Makefile | ||
| index 6b347bd..d3ba762 100644 | ||
| --- a/src/patch/Makefile | ||
| +++ b/src/patch/Makefile | ||
| @@ -1,5 +1,5 @@ | ||
| mlpatch : lexer.mll parser.mly patch.ml mlpatch.ml | ||
| - dune build --root $(CURDIR) | ||
| + dune build | ||
|
|
||
| clean : | ||
| - dune clean --root $(CURDIR) | ||
| + dune clean | ||
| -- | ||
| 2.37.3 | ||
|
|
50 changes: 50 additions & 0 deletions
50
opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.19.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,50 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://gitlab.inria.fr/fbesson/itauto" | ||
| dev-repo: "git+https://gitlab.inria.fr/fbesson/itauto.git" | ||
| authors: ["Frédéric Besson"] | ||
| bug-reports: ["[email protected]" "https://gitlab.inria.fr/fbesson/itauto/-/issues"] | ||
| license: "MIT" | ||
| synopsis: "Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq" | ||
| description: """ | ||
| itauto is a reflexive intuitionistic SAT solver parameterised by a theory module. | ||
| When run inside Coq, the theory module wraps an arbitrary Coq tactic, e.g., the lia | ||
| solver for linear arithmetic or the congruence solver for uninterpreted function symbols | ||
| and constructors. Using a black-box Nelson-Oppen scheme for combination of theories, | ||
| itauto also provides an SMT-like tactic for propositional reasoning modulo the solvers for | ||
| both arithmetic and function symbols. | ||
| """ | ||
|
|
||
| patches: [ | ||
| "0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch" | ||
| ] | ||
| build: [ | ||
| [make "-j%{jobs}%"] | ||
| ] | ||
| install: [make "install"] | ||
| depends: [ | ||
| "ocaml" {>= "4.9~"} | ||
| "coq" {>= "8.19" & < "8.20"} | ||
| "dune" {>= "2.9"} | ||
| ] | ||
| depopts: [ "ocamlformat" {build} ] | ||
|
|
||
| tags: [ | ||
| "category:Miscellaneous/Coq Extensions" | ||
| "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" | ||
| "keyword:integers" | ||
| "keyword:SAT" | ||
| "keyword:SMT" | ||
| "keyword:Nelson-Oppen" | ||
| "keyword:automation" | ||
| "logpath:Cdcl" | ||
| "date:2024-01-03" | ||
| ] | ||
|
|
||
| url { | ||
| src: "https://gitlab.inria.fr/fbesson/itauto/-/archive/8.19.0/itauto-8.19.0.tar.gz" | ||
| checksum: [ | ||
| "md5=95c1617377a2a60f0db72f9893e7149c" | ||
| "sha512=9a5f92dde1cadd7ef70022b5289462d0beadd451e92a42a390dd460e4851f0c85204c97209a3dc0b93cbdfea48131444f3673df34d2021787d807e51cad1d434" | ||
| ] | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| authors: "MSR" | ||
| homepage: "https://github.com/Z3prover/z3" | ||
| bug-reports: "https://github.com/Z3prover/z3/issues" | ||
| license: "MIT" | ||
| dev-repo: "git+https://github.com/Z3prover/z3.git" | ||
| # OK, this is really ugly, but it is quite hard to do this via z3's make system | ||
| # using an already installed opam z3. | ||
| # Also this should be quite robust with just source 2 files and opam knowns the | ||
| # library folder better than any configure script. | ||
| build: [ | ||
| [ "g++" | ||
| "-I./src/api/c++" | ||
| "-I./src/api" | ||
| "-std=c++11" | ||
| "-L%{lib}%/stublibs" | ||
| "-o" "z3_tptp" | ||
| "examples/tptp/tptp5.cpp" "examples/tptp/tptp5.lex.cpp" | ||
| "-lz3" | ||
| "-Wl,-rpath" | ||
| "-Wl,%{lib}%/stublibs" | ||
| ] | ||
| ] | ||
| install: [ "cp" "z3_tptp" "%{bin}%/z3_tptp" ] | ||
| depends: [ | ||
| "z3" { >= "4.13.0" & < "4.13.1~" } | ||
| "conf-g++" {build} | ||
| ] | ||
| synopsis: "TPTP front end for Z3 solver" | ||
| url { | ||
| src: "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.0.tar.gz" | ||
| checksum: [ | ||
| "sha256=01bcc61c8362e37bb89fd2430f7e3385e86df7915019bd2ce45de9d9bd934502" | ||
| "sha512=8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd" | ||
| ] | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters