diff options
Diffstat (limited to 'pkgs/applications/science/logic')
8 files changed, 16 insertions, 187 deletions
diff --git a/pkgs/applications/science/logic/acgtk/default.nix b/pkgs/applications/science/logic/acgtk/default.nix index b787a4e7a01c..729aef4e21c2 100644 --- a/pkgs/applications/science/logic/acgtk/default.nix +++ b/pkgs/applications/science/logic/acgtk/default.nix @@ -1,57 +1,27 @@ -{ stdenv, fetchurl, ocamlPackages, - buildBytecode ? true, - buildNative ? true, - installExamples ? true, - installEmacsMode ? true }: - -let inherit (stdenv.lib) versionAtLeast optionalString; in - -let inherit (ocamlPackages) ocaml camlp4; in - -assert buildBytecode || buildNative; +{ stdenv, fetchurl, dune, ocamlPackages }: stdenv.mkDerivation { - name = "acgtk-1.3.1"; + name = "acgtk-1.5.0"; src = fetchurl { - url = http://calligramme.loria.fr/acg/software/acg-1.3.1-20170303.tar.gz; - sha256 = "1hhrf6bx2x2wbv5ldn4fnxhpr9lyrj3zh1vcnx8wf8f06ih4rzfq"; + url = http://calligramme.loria.fr/acg/software/acg-1.5.0-20181019.tar.gz; + sha256 = "14n003gxzw5w79hlpw1ja4nq97jqf9zqyg00ihvpxw4bv9jlm8jm"; }; - buildInputs = with ocamlPackages; [ - ocaml findlib camlp4 ansiterminal biniou bolt cairo2 dypgen easy-format ocf yojson - ]; - - patches = [ ./install-emacs-to-site-lisp.patch - ./use-nix-ocaml-byteflags.patch ]; - - postPatch = optionalString (camlp4 != null) '' - substituteInPlace src/Makefile.master.in \ - --replace "+camlp4" "${camlp4}/lib/ocaml/${ocaml.version}/site-lib/camlp4/" - '' + optionalString (versionAtLeast (stdenv.lib.getVersion ocamlPackages.yojson) "1.4") '' - substituteInPlace src/scripting/Makefile.in --replace yojson.cmo yojson.cma - ''; - - # The bytecode executable is dependent on the dynamic library provided by - # ANSITerminal. We can use the -dllpath flag of ocamlc (analogous to - # -rpath) to make sure that ocamlrun is able to link the library at - # runtime and that Nix detects a runtime dependency. - NIX_OCAML_BYTEFLAGS = "-dllpath ${ocamlPackages.ansiterminal}/lib/ocaml/${ocaml.version}/site-lib/ANSITerminal"; + buildInputs = [ dune ] ++ (with ocamlPackages; [ + ocaml findlib ansiterminal cairo2 fmt logs menhir mtime ocf + ]); - buildFlags = optionalString buildBytecode "byte" - + " " - + optionalString buildNative "opt"; + buildPhase = "dune build"; - installTargets = "install" - + " " + optionalString installExamples "install-examples" - + " " + optionalString installEmacsMode "install-emacs"; + inherit (dune) installPhase; meta = with stdenv.lib; { homepage = http://calligramme.loria.fr/acg/; description = "A toolkit for developing ACG signatures and lexicon"; license = licenses.cecill20; - platforms = ocaml.meta.platforms or []; + inherit (ocamlPackages.ocaml.meta) platforms; maintainers = [ maintainers.jirkamarsik ]; }; } diff --git a/pkgs/applications/science/logic/acgtk/install-emacs-to-site-lisp.patch b/pkgs/applications/science/logic/acgtk/install-emacs-to-site-lisp.patch deleted file mode 100644 index 43ddd20b4a39..000000000000 --- a/pkgs/applications/science/logic/acgtk/install-emacs-to-site-lisp.patch +++ /dev/null @@ -1,23 +0,0 @@ ---- acg-1.1-20140905/Makefile.in 2014-10-24 15:21:39.442287208 +0200 -+++ acg-1.1-20140905/Makefile.in.new 2014-10-24 15:24:58.557117228 +0200 -@@ -35,6 +35,7 @@ - ACGC_DIR=src/acg-data - - DATA_DIR=@datarootdir@/acgtk -+EMACS_DIR=@prefix@/share/emacs/site-lisp - - - -@@ -82,10 +83,10 @@ - rm -r $(DATA_DIR) - - install-emacs: -- mkdir -p $(DATA_DIR) && cp -r emacs $(DATA_DIR)/. -+ mkdir -p $(EMACS_DIR) && cp emacs/acg.el $(EMACS_DIR) - - uninstall-emacs: -- rm -rf $(DATA_DIR)/emacs -+ rm -rf $(EMACS_DIR)/emacs - - install-examples: - mkdir -p $(DATA_DIR) && cp -r examples $(DATA_DIR)/. diff --git a/pkgs/applications/science/logic/acgtk/use-nix-ocaml-byteflags.patch b/pkgs/applications/science/logic/acgtk/use-nix-ocaml-byteflags.patch deleted file mode 100644 index 26ade37e4521..000000000000 --- a/pkgs/applications/science/logic/acgtk/use-nix-ocaml-byteflags.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- acg-1.1-20140905/src/Makefile.master.in 2014-10-27 10:59:42.263382081 +0100 -+++ acg-1.1-20140905/src/Makefile.master.in.new 2014-10-27 10:59:59.683597972 +0100 -@@ -23,7 +23,7 @@ - # All warnings are treated as errors - WARNINGS = @OCAML09WARNINGS@ -warn-error A - COMMONFLAGS= $(WARNINGS) @TYPES@ --BYTEFLAGS = $(COMMONFLAGS) $(DEBUGFLAG) -+BYTEFLAGS = $(COMMONFLAGS) $(DEBUGFLAG) $(NIX_OCAML_BYTEFLAGS) - OPTFLAGS = $(COMMONFLAGS) - LFLAGS= -a - diff --git a/pkgs/applications/science/logic/coq/8.4.nix b/pkgs/applications/science/logic/coq/8.4.nix deleted file mode 100644 index c3da1205ab0c..000000000000 --- a/pkgs/applications/science/logic/coq/8.4.nix +++ /dev/null @@ -1,97 +0,0 @@ -# - coqide compilation can be disabled by setting lablgtk to null; -# - The csdp program used for the Micromega tactic is statically referenced. -# However, coq can build without csdp by setting it to null. -# In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found. - -{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}: - -let - version = "8.4pl6"; - coq-version = "8.4"; - buildIde = lablgtk != null; - ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; - csdpPatch = if csdp != null then '' - substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" - substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" - '' else ""; - -self = -stdenv.mkDerivation { - name = "coq-${version}"; - - inherit coq-version; - inherit ocaml camlp5; - - src = fetchurl { - url = "https://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz"; - sha256 = "1mpbj4yf36kpjg2v2sln12i8dzqn8rag6fd07hslj2lpm4qs4h55"; - }; - - nativeBuildInputs = [ pkgconfig ]; - buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ]; - - patches = [ ./configure.patch ]; - - postPatch = '' - UNAME=$(type -tp uname) - RM=$(type -tp rm) - substituteInPlace configure --replace "/bin/uname" "$UNAME" - substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" - ${csdpPatch} - ''; - - preConfigure = '' - configureFlagsArray=( - -opt - -camldir ${ocaml}/bin - -camlp5dir $(ocamlfind query camlp5) - ${ideFlags} - ) - ''; - - prefixKey = "-prefix "; - - buildFlags = "revision coq coqide"; - - setupHook = writeText "setupHook.sh" '' - addCoqPath () { - if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then - export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/" - fi - } - - addEnvHooks "$targetOffset" addCoqPath - ''; - - passthru = { - inherit findlib; - emacsBufferSetup = pkgs: '' - ; Propagate coq paths to children - (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") - (inherit-local-permanent coq-dependency-analyzer "${self}/bin/coqdep") - (inherit-local-permanent coq-compiler "${self}/bin/coqc") - ; If the coq-library path was already set, re-set it based on our current coq - (when (fboundp 'get-coq-library-directory) - (inherit-local-permanent coq-library-directory (get-coq-library-directory)) - (coq-prog-args)) - (mapc (lambda (arg) - (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib")) - (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) - ''; - }; - - meta = with stdenv.lib; { - description = "Formal proof management system"; - longDescription = '' - Coq is a formal proof management system. It provides a formal language - to write mathematical definitions, executable algorithms and theorems - together with an environment for semi-interactive development of - machine-checked proofs. - ''; - homepage = http://coq.inria.fr; - license = licenses.lgpl21; - branch = coq-version; - maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; - platforms = platforms.unix; - }; -}; in self diff --git a/pkgs/applications/science/logic/coq/configure.patch b/pkgs/applications/science/logic/coq/configure.patch deleted file mode 100644 index aa38ce06e92b..000000000000 --- a/pkgs/applications/science/logic/coq/configure.patch +++ /dev/null @@ -1,11 +0,0 @@ -diff -Nuar coq-8.3pl3-orig/configure coq-8.3pl3/configure ---- coq-8.3pl3-orig/configure 2011-12-19 22:57:30.000000000 +0100 -+++ coq-8.3pl3/configure 2012-03-17 16:38:16.000000000 +0100 -@@ -395,7 +395,6 @@ - ocamlyaccexec=$CAMLBIN/ocamlyacc - ocamlmktopexec=$CAMLBIN/ocamlmktop - ocamlmklibexec=$CAMLBIN/ocamlmklib -- camlp4oexec=$CAMLBIN/camlp4o - esac - - if test ! -f "$CAMLC" ; then diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 040d722f9410..5fab9788a94a 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -25,6 +25,7 @@ let "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; + "8.9+beta1" = "1yxv2klqal3mh6symi3gc6gv3xm684zlld2c0b6ijhjmp865cin8"; }."${version}"; coq-version = builtins.substring 0 3 version; ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix index 3121a83e5b98..0ab08db67465 100644 --- a/pkgs/applications/science/logic/yices/default.nix +++ b/pkgs/applications/science/logic/yices/default.nix @@ -2,12 +2,12 @@ stdenv.mkDerivation rec { name = "yices-${version}"; - version = "2.6.0"; + version = "2.6.1"; src = fetchurl { url = "https://github.com/SRI-CSL/yices2/archive/Yices-${version}.tar.gz"; name = "${name}-src.tar.gz"; - sha256 = "10ikq7ib8jhx7hlxfm6mp5qg6r8dflqs8242q5zaicn80qixpm12"; + sha256 = "14xvflv14qn8ssm8rklvckp6l1q94vn49qz2snz73j40nwzshaww"; }; nativeBuildInputs = [ autoreconfHook ]; diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 1cbe914779e6..f7d67d82cbc8 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -2,13 +2,13 @@ stdenv.mkDerivation rec { name = "z3-${version}"; - version = "4.7.1"; + version = "4.8.1"; src = fetchFromGitHub { owner = "Z3Prover"; repo = "z3"; - rev = "3b1b82bef05a1b5fd69ece79c80a95fb6d72a990"; - sha256 = "1s850r6qifwl83zzgvrb5l0jigvmymzpv18ph71hg2bcpk7kjw3d"; + rev = name; + sha256 = "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"; }; buildInputs = [ python fixDarwinDylibNames ]; |