sad: remove old, unmaintained package
The package isn't maintained and hasn't been exposed for a while. Meanwhile there's been added a new package with the same name. This change doesn't touch the new package.
This commit is contained in:
Felix Schröter
@@ -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
|
||||
};
|
||||
}
|
||||
@@ -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
|
||||
@@ -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.
|
||||
@@ -23484,14 +23484,6 @@ with pkgs;
|
||||
|
||||
s2geometry = callPackage ../development/libraries/s2geometry { };
|
||||
|
||||
/* This package references ghc844, which we no longer have. Unfortunately, I
|
||||
have been unable to mark it as "broken" in a way that the ofBorg bot
|
||||
recognizes. Since I don't want to merge code into master that generates
|
||||
evaluation errors, I have no other idea but to comment it out entirely.
|
||||
|
||||
sad = callPackage ../applications/science/logic/sad { };
|
||||
*/
|
||||
|
||||
safefile = callPackage ../development/libraries/safefile { };
|
||||
|
||||
sbc = callPackage ../development/libraries/sbc { };
|
||||
|
||||
Reference in New Issue
Block a user