From c13f189b19e16e25d49152ed176b2f62b65057dc Mon Sep 17 00:00:00 2001 From: Shea Levy Date: Mon, 11 May 2015 06:41:53 -0400 Subject: [PATCH] ats-extsolve: bump --- .../compilers/ats-extsolve/default.nix | 11 +- .../compilers/ats-extsolve/misc-fixes.patch | 136 ------------------ 2 files changed, 5 insertions(+), 142 deletions(-) delete mode 100644 pkgs/development/compilers/ats-extsolve/misc-fixes.patch diff --git a/pkgs/development/compilers/ats-extsolve/default.nix b/pkgs/development/compilers/ats-extsolve/default.nix index 9cd6d3adb324..c1a7f2882a0a 100644 --- a/pkgs/development/compilers/ats-extsolve/default.nix +++ b/pkgs/development/compilers/ats-extsolve/default.nix @@ -1,22 +1,21 @@ { stdenv, fetchurl, ats2, python, z3, pkgconfig, json_c }: stdenv.mkDerivation { - name = "ats-extsolve-0pre6a9b752"; + name = "ats-extsolve-0pre11177d9"; buildInputs = [ python z3 ats2 pkgconfig json_c ]; src = fetchurl { - url = "https://github.com/githwxi/ATS-Postiats-contrib/archive/6a9b752efb8af1e4f77213f9e81fc2b7fa050877.tar.gz"; - sha256 = "1zz4fqjm1rdvpm0m0sdck6vx55iiqlk2p8z078fca2q9xyxqjkqd"; + url = "https://github.com/wdblair/ATS-Postiats-contrib/archive/11177d9194b852392d5e92e67d0ecc7b6abc02bf.tar.gz"; + sha256 = "12fhlcpq5b4pc3h21w1i7yv1ymrll2g4zlf1pvg0v8cr6aa6i813"; }; postUnpack = '' - export PATSHOMERELOC="$PWD/$sourceRoot"; + export PATSHOMERELOC="$PWD/$sourceRoot" export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE -I$PATSHOMERELOC" + export INCLUDE_ATS="-IATS $PATSHOMERELOC" ''; - patches = [ ./misc-fixes.patch ]; - preBuild = "cd projects/MEDIUM/ATS-extsolve"; buildFlags = [ "setup" "patsolve" ]; diff --git a/pkgs/development/compilers/ats-extsolve/misc-fixes.patch b/pkgs/development/compilers/ats-extsolve/misc-fixes.patch deleted file mode 100644 index 8775bb83ba4c..000000000000 --- a/pkgs/development/compilers/ats-extsolve/misc-fixes.patch +++ /dev/null @@ -1,136 +0,0 @@ -From bfc7216250e666a59e304f3b7518f8b0bccccbae Mon Sep 17 00:00:00 2001 -From: Shea Levy -Date: Thu, 30 Apr 2015 16:50:47 -0400 -Subject: [PATCH] Add missing case in fprint_s2rt - ---- - projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats | 1 + - 1 file changed, 1 insertion(+) - -diff --git a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats -index a841b5f..5bc28d7 100644 ---- a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats -+++ b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats -@@ -113,6 +113,7 @@ case+ s2t0 of - | S2RTfun (args, ret) => fprint (out, "S2RTfun()") - | S2RTtup () => fprint (out, "S2RTtup()") - | S2RTerr () => fprint (out, "S2RTerr()") -+| S2RTuninterp (str) => fprint! (out, "S2RTuninterp(", str, ")") - // - | S2RTignored () => fprint (out, "S2RTignored()") - // -From 9d4c7669d0d3bc8725648684391a2962ed5a922e Mon Sep 17 00:00:00 2001 -From: Shea Levy -Date: Thu, 30 Apr 2015 17:13:35 -0400 -Subject: [PATCH] ATS-extsolve: Get rid of verbose . overload - ---- - projects/MEDIUM/ATS-extsolve/solving/solver.dats | 2 +- - projects/MEDIUM/ATS-extsolve/solving/solver.sats | 6 ------ - 2 files changed, 1 insertion(+), 7 deletions(-) - -diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.dats b/projects/MEDIUM/ATS-extsolve/solving/solver.dats -index 8446cd5..f2f77b4 100644 ---- a/projects/MEDIUM/ATS-extsolve/solving/solver.dats -+++ b/projects/MEDIUM/ATS-extsolve/solving/solver.dats -@@ -250,7 +250,7 @@ end // end of [c3nstr_solve_main] - implement c3nstr_solve (c3t, scripts, verbose) = let - var env : smtenv - val _ = smtenv_nil (env) -- val () = env.verbose (verbose) -+ val () = smtenv_set_verbose(env, verbose) - val () = - case+ scripts of - | list_nil () => () -diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.sats b/projects/MEDIUM/ATS-extsolve/solving/solver.sats -index e43a028..dae452c 100644 ---- a/projects/MEDIUM/ATS-extsolve/solving/solver.sats -+++ b/projects/MEDIUM/ATS-extsolve/solving/solver.sats -@@ -39,14 +39,8 @@ fun smtenv_load_scripts (env: &smtenv, scripts: List0(string)): void - - fun smtenv_get_solver (env: &smtenv): solver - --fun smtenv_get_verbose (env: &smtenv): bool -- --overload .verbose with smtenv_get_verbose -- - fun smtenv_set_verbose (env: &smtenv, verbose: bool): void - --overload .verbose with smtenv_set_verbose -- - fun formula_cst (s2c: s2cst): formula - - (* ****** ****** *) -From e3473a8d9dc7c56cda1111a439db7123254d00b4 Mon Sep 17 00:00:00 2001 -From: Shea Levy -Date: Thu, 30 Apr 2015 18:09:33 -0400 -Subject: [PATCH 1/2] solver_smt.dats: Don't use mapfree on linear list of - non-linear values - ---- - projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats | 5 +++-- - 1 file changed, 3 insertions(+), 2 deletions(-) - -diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats -index 04055b9..b49602d 100644 ---- a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats -+++ b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats -@@ -348,7 +348,7 @@ in - // - val () = assertloc (length(pairs) > 0) - // -- implement list_vt_mapfree$fopr<@(s2exp,s2exp)>(x) = let -+ implement list_vt_map$fopr<@(s2exp,s2exp)>(x) = let - val (pf, fpf | Env) = $UN.ptr1_vtake{smtenv}(addr@ env) - val met = formula_make (!Env, x.0) - val bound = formula_make (!Env, x.1) -@@ -362,7 +362,8 @@ in - end - // - val assertions = -- list_vt_mapfree<(s2exp,s2exp)> (pairs) -+ list_vt_map<(s2exp,s2exp)> (pairs) -+ val () = list_vt_free(pairs) - // - implement - list_vt_fold$init (x) = x - -From 50de956561e6bf43190d7efb385bb6da658f1637 Mon Sep 17 00:00:00 2001 -From: Shea Levy -Date: Thu, 30 Apr 2015 18:18:56 -0400 -Subject: [PATCH 2/2] ats-extsolve/main.dats: Don't use mapfree on linear list - of non-linear values - ---- - projects/MEDIUM/ATS-extsolve/main.dats | 7 ++++--- - 1 file changed, 4 insertions(+), 3 deletions(-) - -diff --git a/projects/MEDIUM/ATS-extsolve/main.dats b/projects/MEDIUM/ATS-extsolve/main.dats -index ac30ca0..930697d 100644 ---- a/projects/MEDIUM/ATS-extsolve/main.dats -+++ b/projects/MEDIUM/ATS-extsolve/main.dats -@@ -34,7 +34,7 @@ dynload "commarg.dats" - - (* ****** ****** *) - --overload mapfree with list_vt_mapfree -+overload map with list_vt_map - overload filter with list_vt_filter - - (* ****** ****** *) -@@ -56,12 +56,13 @@ implement main0 (argc, argv) = let - | Script (s) => true - | _ =>> false - implement -- list_vt_mapfree$fopr (x) = -+ list_vt_map$fopr (x) = - case- x of - | Script (s) => s - // - val scriptargs = filter (list_vt_copy (args)) -- val scripts = mapfree (scriptargs) -+ val scripts = map (scriptargs) -+ val () = list_vt_free (scriptargs) - // - implement - list_find$pred (x) =