Merge pull request #227226 from felschr/remove-sad

{ 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/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 -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.

  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 { };