diff options
| author | Mort Yao | 2019-10-20 16:48:17 +0200 |
|---|---|---|
| committer | Mort Yao | 2019-10-20 16:48:17 +0200 |
| commit | ab0d11b8f12927433ec586b55501d39b5c956d3b (patch) | |
| tree | 39d4b5e00e71f0e815ed3035db0cfa1e5e5ad88b | |
| parent | f705f3b623afa868566a40f52a4bbdd5438dc00d (diff) | |
| download | aur-ab0d11b8f12927433ec586b55501d39b5c956d3b.tar.gz | |
fstar 0.9.7.0-2
| -rw-r--r-- | .SRCINFO | 6 | ||||
| -rw-r--r-- | PKGBUILD | 14 | ||||
| -rw-r--r-- | fix-ocaml-4.08.patch | 34 |
3 files changed, 49 insertions, 5 deletions
@@ -1,9 +1,9 @@ # Generated by mksrcinfo v8 -# Sat Oct 19 23:57:04 UTC 2019 +# Sun Oct 20 14:41:54 UTC 2019 pkgbase = fstar pkgdesc = A Higher-Order Effectful Language Designed for Program Verification pkgver = 0.9.7.0 - pkgrel = 1 + pkgrel = 2 url = https://fstar-lang.org/ arch = i686 arch = x86_64 @@ -28,7 +28,9 @@ pkgbase = fstar conflicts = fstar-bin conflicts = fstar-git source = https://github.com/FStarLang/FStar/archive/v0.9.7.0-alpha1.zip + source = fix-ocaml-4.08.patch md5sums = 754ecb3d2f6c234c78537707a87e6db2 + md5sums = 1bbf449622e26f6ea2d414b6d9866e52 pkgname = fstar @@ -3,7 +3,7 @@ pkgname=fstar pkgver=0.9.7.0 _subver=-alpha1 -pkgrel=1 +pkgrel=2 pkgdesc='A Higher-Order Effectful Language Designed for Program Verification' url='https://fstar-lang.org/' license=('Apache') @@ -12,8 +12,16 @@ depends=('z3-git') makedepends=('ocaml>=4.03' 'ocaml-findlib' 'ocaml-num' 'ocaml-batteries' 'ocaml-stdint' 'zarith' 'ocaml-yojson' 'ocaml-fileutils' 'ocaml-pprint' 'ocaml-menhir' 'ulex-git' 'ocaml-migrate-parsetree' 'ocaml-ppx_deriving' 'ocaml-ppx_deriving_yojson' 'ocaml-process') provides=('fstar') conflicts=('fstar-bin' 'fstar-git') -source=("https://github.com/FStarLang/FStar/archive/v$pkgver$_subver.zip") -md5sums=('754ecb3d2f6c234c78537707a87e6db2') +source=("https://github.com/FStarLang/FStar/archive/v$pkgver$_subver.zip" + fix-ocaml-4.08.patch) +md5sums=('754ecb3d2f6c234c78537707a87e6db2' + '1bbf449622e26f6ea2d414b6d9866e52') + +prepare() { + cd "FStar-$pkgver$_subver" + + patch -Np1 -i ../fix-ocaml-4.08.patch +} build() { cd "FStar-$pkgver$_subver" diff --git a/fix-ocaml-4.08.patch b/fix-ocaml-4.08.patch new file mode 100644 index 000000000000..725aeae88a99 --- /dev/null +++ b/fix-ocaml-4.08.patch @@ -0,0 +1,34 @@ + +--- FStar-0.9.7.0-alpha1/src/tactics/ml/FStar_Tactics_Load.ml2 2019-10-20 16:32:25.391276735 +0200 ++++ FStar-0.9.7.0-alpha1/src/tactics/ml/FStar_Tactics_Load.ml 2019-10-20 16:33:25.817940824 +0200 +@@ -5,21 +5,6 @@ + + let loaded_taclib = ref false + +-(* We had weird failures, so don't trust in Dynlink.error_message *) +-let error_message : Dynlink.error -> string = +- fun e -> +- let s = match e with +- | Not_a_bytecode_file _ -> "Not_a_bytecode_file" +- | Inconsistent_import _ -> "Inconsistent_import" +- | Unavailable_unit _ -> "Unavailable_unit" +- | Unsafe_file -> "Unsafe_file" +- | Linking_error _ -> "Linking_error" +- | Corrupted_interface _ -> "Corrupted_interface" +- | File_not_found _ -> "File_not_found" +- | Cannot_open_dll _ -> "Cannot_open_dll" +- | Inconsistent_implementation _ -> "Inconsistent_implementation" +- in s ^ ": " ^ Dynlink.error_message e +- + let find_taclib () = + let r = Process.run "ocamlfind" [| "query"; "fstar-tactics-lib" |] in + match r with +@@ -35,7 +20,7 @@ + print_string ("Loading plugin from " ^ fname ^ "\n"); + Dynlink.loadfile fname + with Dynlink.Error e -> +- failwith (U.format2 "Dynlinking %s failed: %s" fname (error_message e)) in ++ failwith (U.format2 "Dynlinking %s failed: %s" fname (Dynlink.error_message e)) in + + if not !loaded_taclib then begin + dynlink (find_taclib () ^ "/fstartaclib.cmxs"); |