diff options
Diffstat (limited to 'pkgs/applications/science/logic')
| -rw-r--r-- | pkgs/applications/science/logic/sad/default.nix | 41 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/sad/monoid.patch | 51 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/sad/patch.patch | 200 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/tlaplus/default.nix | 4 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/z3/default.nix | 4 |
5 files changed, 4 insertions, 296 deletions
diff --git a/pkgs/applications/science/logic/sad/default.nix b/pkgs/applications/science/logic/sad/default.nix deleted file mode 100644 index a509d70ed4624..0000000000000 --- a/pkgs/applications/science/logic/sad/default.nix +++ /dev/null @@ -1,41 +0,0 @@ -{ lib, stdenv, fetchurl, haskell, spass }: - -stdenv.mkDerivation rec { - pname = "system-for-automated-deduction"; - version = "2.3.25"; - src = fetchurl { - url = "http://nevidal.org/download/sad-${version}.tar.gz"; - sha256 = "10jd93xgarik7xwys5lq7fx4vqp7c0yg1gfin9cqfch1k1v8ap4b"; - }; - buildInputs = [ haskell.compiler.ghc844 spass ]; - patches = [ - ./patch.patch - # Since the LTS 12.0 update, <> is an operator in Prelude, colliding with - # the <> operator with a different meaning defined by this package - ./monoid.patch - ]; - postPatch = '' - substituteInPlace Alice/Main.hs --replace init.opt $out/init.opt - ''; - installPhase = '' - mkdir -p $out/{bin,provers} - install alice $out/bin - install provers/moses $out/provers - substituteAll provers/provers.dat $out/provers/provers.dat - substituteAll init.opt $out/init.opt - cp -r examples $out - ''; - inherit spass; - meta = { - description = "A program for automated proving of mathematical texts"; - longDescription = '' - The system for automated deduction is intended for automated processing of formal mathematical texts - written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language - ''; - license = lib.licenses.gpl3Plus; - maintainers = [ lib.maintainers.schmitthenner ]; - homepage = "http://nevidal.org/sad.en.html"; - platforms = lib.platforms.linux; - broken = true; # ghc-8.4.4 is gone from Nixpkgs - }; -} diff --git a/pkgs/applications/science/logic/sad/monoid.patch b/pkgs/applications/science/logic/sad/monoid.patch deleted file mode 100644 index da9c21bcae918..0000000000000 --- a/pkgs/applications/science/logic/sad/monoid.patch +++ /dev/null @@ -1,51 +0,0 @@ -diff --git a/Alice/Core/Check.hs b/Alice/Core/Check.hs -index 0700fa0388f..69815864710 100644 ---- a/Alice/Core/Check.hs -+++ b/Alice/Core/Check.hs -@@ -18,8 +18,12 @@ - - along with this program. If not, see <http://www.gnu.org/licenses/>. - -} - -+{-# LANGUAGE NoImplicitPrelude #-} -+ - module Alice.Core.Check (fillDef) where - -+import Prelude hiding ((<>)) -+ - import Control.Monad - import Data.Maybe - -diff --git a/Alice/Core/Reason.hs b/Alice/Core/Reason.hs -index c361bcf220d..4e493d8c91b 100644 ---- a/Alice/Core/Reason.hs -+++ b/Alice/Core/Reason.hs -@@ -17,9 +17,12 @@ - - You should have received a copy of the GNU General Public License - - along with this program. If not, see <http://www.gnu.org/licenses/>. - -} -+{-# LANGUAGE NoImplicitPrelude #-} - - module Alice.Core.Reason where - -+import Prelude hiding ((<>)) -+ - import Control.Monad - - import Alice.Core.Base -diff --git a/Alice/Core/Verify.hs b/Alice/Core/Verify.hs -index 4f8550bdf11..0f59d135b16 100644 ---- a/Alice/Core/Verify.hs -+++ b/Alice/Core/Verify.hs -@@ -18,8 +18,12 @@ - - along with this program. If not, see <http://www.gnu.org/licenses/>. - -} - -+{-# LANGUAGE NoImplicitPrelude #-} -+ - module Alice.Core.Verify (verify) where - -+import Prelude hiding ((<>)) -+ - import Control.Monad - import Data.IORef - import Data.Maybe diff --git a/pkgs/applications/science/logic/sad/patch.patch b/pkgs/applications/science/logic/sad/patch.patch deleted file mode 100644 index a5b1d61770837..0000000000000 --- a/pkgs/applications/science/logic/sad/patch.patch +++ /dev/null @@ -1,200 +0,0 @@ -diff -aur serious/sad-2.3-25/Alice/Core/Base.hs sad-2.3-25/Alice/Core/Base.hs ---- serious/sad-2.3-25/Alice/Core/Base.hs 2008-03-29 18:24:12.000000000 +0000 -+++ sad-2.3-25/Alice/Core/Base.hs 2015-11-27 06:38:28.740840823 +0000 -@@ -21,6 +21,7 @@ - module Alice.Core.Base where - - import Control.Monad -+import Control.Applicative - import Data.IORef - import Data.List - import Data.Time -@@ -61,10 +62,21 @@ - type CRMC a b = IORef RState -> IO a -> (b -> IO a) -> IO a - newtype CRM b = CRM { runCRM :: forall a . CRMC a b } - -+instance Functor CRM where -+ fmap = liftM -+ -+instance Applicative CRM where -+ pure = return -+ (<*>) = ap -+ - instance Monad CRM where - return r = CRM $ \ _ _ k -> k r - m >>= n = CRM $ \ s z k -> runCRM m s z (\ r -> runCRM (n r) s z k) - -+instance Alternative CRM where -+ (<|>) = mplus -+ empty = mzero -+ - instance MonadPlus CRM where - mzero = CRM $ \ _ z _ -> z - mplus m n = CRM $ \ s z k -> runCRM m s (runCRM n s z k) k -diff -aur serious/sad-2.3-25/Alice/Core/Thesis.hs sad-2.3-25/Alice/Core/Thesis.hs ---- serious/sad-2.3-25/Alice/Core/Thesis.hs 2008-03-05 13:10:50.000000000 +0000 -+++ sad-2.3-25/Alice/Core/Thesis.hs 2015-11-27 06:35:08.311015166 +0000 -@@ -21,6 +21,7 @@ - module Alice.Core.Thesis (thesis) where - - import Control.Monad -+import Control.Applicative - import Data.List - import Data.Maybe - -@@ -126,11 +127,22 @@ - - newtype TM res = TM { runTM :: [String] -> [([String], res)] } - -+instance Functor TM where -+ fmap = liftM -+ -+instance Applicative TM where -+ pure = return -+ (<*>) = ap -+ - instance Monad TM where - return r = TM $ \ s -> [(s, r)] - m >>= k = TM $ \ s -> concatMap apply (runTM m s) - where apply (s, r) = runTM (k r) s - -+instance Alternative TM where -+ (<|>) = mplus -+ empty = mzero -+ - instance MonadPlus TM where - mzero = TM $ \ _ -> [] - mplus m k = TM $ \ s -> runTM m s ++ runTM k s -diff -aur serious/sad-2.3-25/Alice/Export/Base.hs sad-2.3-25/Alice/Export/Base.hs ---- serious/sad-2.3-25/Alice/Export/Base.hs 2008-03-09 09:36:39.000000000 +0000 -+++ sad-2.3-25/Alice/Export/Base.hs 2015-11-27 06:32:47.782738005 +0000 -@@ -39,7 +39,7 @@ - -- Database reader - - readPrDB :: String -> IO [Prover] --readPrDB file = do inp <- catch (readFile file) $ die . ioeGetErrorString -+readPrDB file = do inp <- catchIOError (readFile file) $ die . ioeGetErrorString - - let dws = dropWhile isSpace - cln = reverse . dws . reverse . dws -diff -aur serious/sad-2.3-25/Alice/Export/Prover.hs sad-2.3-25/Alice/Export/Prover.hs ---- serious/sad-2.3-25/Alice/Export/Prover.hs 2008-03-09 09:36:39.000000000 +0000 -+++ sad-2.3-25/Alice/Export/Prover.hs 2015-11-27 06:36:47.632919161 +0000 -@@ -60,7 +60,7 @@ - when (askIB IBPdmp False ins) $ putStrLn tsk - - seq (length tsk) $ return $ -- do (wh,rh,eh,ph) <- catch run -+ do (wh,rh,eh,ph) <- catchIOError run - $ \ e -> die $ "run error: " ++ ioeGetErrorString e - - hPutStrLn wh tsk ; hClose wh -diff -aur serious/sad-2.3-25/Alice/ForTheL/Base.hs sad-2.3-25/Alice/ForTheL/Base.hs ---- serious/sad-2.3-25/Alice/ForTheL/Base.hs 2008-03-09 09:36:39.000000000 +0000 -+++ sad-2.3-25/Alice/ForTheL/Base.hs 2015-11-27 06:31:51.921230428 +0000 -@@ -226,7 +226,7 @@ - varlist = do vs <- chainEx (char ',') var - nodups vs ; return vs - --nodups vs = unless (null $ dups vs) $ -+nodups vs = unless ((null :: [a] -> Bool) $ dups vs) $ - fail $ "duplicate names: " ++ show vs - - hidden = askPS psOffs >>= \ n -> return ('h':show n) -diff -aur serious/sad-2.3-25/Alice/Import/Reader.hs sad-2.3-25/Alice/Import/Reader.hs ---- serious/sad-2.3-25/Alice/Import/Reader.hs 2008-03-09 09:36:39.000000000 +0000 -+++ sad-2.3-25/Alice/Import/Reader.hs 2015-11-27 06:36:41.818866167 +0000 -@@ -24,7 +24,7 @@ - import Control.Monad - import System.IO - import System.IO.Error --import System.Exit -+import System.Exit hiding (die) - - import Alice.Data.Text - import Alice.Data.Instr -@@ -44,7 +44,7 @@ - readInit "" = return [] - - readInit file = -- do input <- catch (readFile file) $ die file . ioeGetErrorString -+ do input <- catchIOError (readFile file) $ die file . ioeGetErrorString - let tkn = tokenize input ; ips = initPS () - inp = ips { psRest = tkn, psFile = file, psLang = "Init" } - liftM fst $ fireLPM instf inp -@@ -74,7 +74,7 @@ - reader lb fs (ps:ss) [TI (InStr ISfile file)] = - do let gfl = if null file then hGetContents stdin - else readFile file -- input <- catch gfl $ die file . ioeGetErrorString -+ input <- catchIOError gfl $ die file . ioeGetErrorString - let tkn = tokenize input - ips = initPS $ (psProp ps) { tvr_expr = [] } - sps = ips { psRest = tkn, psFile = file, psOffs = psOffs ps } -diff -aur serious/sad-2.3-25/Alice/Parser/Base.hs sad-2.3-25/Alice/Parser/Base.hs ---- serious/sad-2.3-25/Alice/Parser/Base.hs 2008-03-09 09:36:40.000000000 +0000 -+++ sad-2.3-25/Alice/Parser/Base.hs 2015-11-27 06:14:28.616734527 +0000 -@@ -20,6 +20,7 @@ - - module Alice.Parser.Base where - -+import Control.Applicative - import Control.Monad - import Data.List - -@@ -45,11 +46,22 @@ - type CPMC a b c = (c -> CPMS a b) -> (String -> CPMS a b) -> CPMS a b - newtype CPM a c = CPM { runCPM :: forall b . CPMC a b c } - -+instance Functor (CPM a) where -+ fmap = liftM -+ -+instance Applicative (CPM a) where -+ pure = return -+ (<*>) = ap -+ - instance Monad (CPM a) where - return r = CPM $ \ k _ -> k r - m >>= n = CPM $ \ k l -> runCPM m (\ b -> runCPM (n b) k l) l - fail e = CPM $ \ _ l -> l e - -+instance Alternative (CPM a) where -+ (<|>) = mplus -+ empty = mzero -+ - instance MonadPlus (CPM a) where - mzero = CPM $ \ _ _ _ z -> z - mplus m n = CPM $ \ k l s -> runCPM m k l s . runCPM n k l s -diff -aur serious/sad-2.3-25/init.opt sad-2.3-25/init.opt ---- serious/sad-2.3-25/init.opt 2007-10-11 15:25:45.000000000 +0000 -+++ sad-2.3-25/init.opt 2015-11-27 07:23:41.372816854 +0000 -@@ -1,6 +1,6 @@ - # Alice init options --[library examples] --[provers provers/provers.dat] -+[library @out@/examples] -+[provers @out@/provers/provers.dat] - [prover spass] - [timelimit 3] - [depthlimit 7] -diff -aur serious/sad-2.3-25/provers/provers.dat sad-2.3-25/provers/provers.dat ---- serious/sad-2.3-25/provers/provers.dat 2008-08-26 21:20:25.000000000 +0000 -+++ sad-2.3-25/provers/provers.dat 2015-11-27 07:24:18.878169702 +0000 -@@ -3,7 +3,7 @@ - Pmoses - LMoses - Fmoses --Cprovers/moses -+C@out@/provers/moses - Yproved in - Nfound unprovable in - Utimeout in -@@ -12,7 +12,7 @@ - Pspass - LSPASS - Fdfg --Cprovers/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d -+C@spass@/bin/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d - YSPASS beiseite: Proof found. - NSPASS beiseite: Completion found. - USPASS beiseite: Ran out of time. diff --git a/pkgs/applications/science/logic/tlaplus/default.nix b/pkgs/applications/science/logic/tlaplus/default.nix index 4572a06d63378..abbcd417693e4 100644 --- a/pkgs/applications/science/logic/tlaplus/default.nix +++ b/pkgs/applications/science/logic/tlaplus/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "tlaplus"; - version = "1.7.2"; + version = "1.7.3"; src = fetchurl { url = "https://github.com/tlaplus/tlaplus/releases/download/v${version}/tla2tools.jar"; - sha256 = "sha256-+hhUPkTtWXSoW9LGDA3BZiCuEXaA6o5pPSaRmZ7ZCyI="; + sha256 = "sha256-5P8V6oH05voSXAgwBDclSxdxdMalrfaNpElkar4IUZ0="; }; nativeBuildInputs = [ makeWrapper ]; diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index f810a5a56739a..e2842d9d15a4f 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -92,8 +92,8 @@ in sha256 = "sha256-ItmtZHDhCeLAVtN7K80dqyAh20o7TM4xk2sTb9QgHvk="; }; z3_4_8 = common { - version = "4.8.15"; - sha256 = "0xkwqz0y5d1lfb6kfqy8wn8n2dqalzf4c8ghmjsajc1bpdl70yc5"; + version = "4.8.17"; + sha256 = "sha256-BSwjgOU9EgCcm18Zx0P9mnoPc9ZeYsJwEu0ffnACa+8="; }; z3_4_8_5 = common { tag = "Z3"; |