diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,176 +1,176 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" isabelle_scala_service 'isabelle.Tools' [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools' isabelle_scala_service 'isabelle.Scala_Functions' isabelle_scala_service 'isabelle.Sessions$File_Format' isabelle_scala_service 'isabelle.Bibtex$File_Format' isabelle_scala_service 'isabelle.ML_Statistics$Handler' isabelle_scala_service 'isabelle.Scala$Handler' isabelle_scala_service 'isabelle.Print_Operation$Handler' isabelle_scala_service 'isabelle.Simplifier_Trace$Handler' isabelle_scala_service 'isabelle.Server_Commands' #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex/document) ### ISABELLE_PDFLATEX="lualatex --file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex" ISABELLE_EPSTOPDF="epstopdf" ### ### Misc path settings ### isabelle_directory '~' isabelle_directory '$ISABELLE_HOME_USER' isabelle_directory '~~' ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER" # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" ISABELLE_DOCS_EXAMPLES="~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_OPEN="xdg-open" ;; macos) ISABELLE_OPEN="open" ;; windows) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" -ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.05.0" +ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.07.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-16.12" ISABELLE_GHC_VERSION="ghc-8.8.4" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/Pure/Admin/build_vampire.scala b/src/Pure/Admin/build_vampire.scala --- a/src/Pure/Admin/build_vampire.scala +++ b/src/Pure/Admin/build_vampire.scala @@ -1,169 +1,171 @@ /* Title: Pure/Admin/build_vampire.scala Author: Makarius Build Isabelle Vampire component from repository. */ package isabelle object Build_Vampire { val default_repository = "https://github.com/vprover/vampire.git" val default_version1 = "4.5.1" val default_version2 = "df87588848db" val default_jobs = 1 def make_component_name(version: String) = "vampire-" + version /* build Vampire */ def build_vampire( repository: String = default_repository, version1: String = default_version1, version2: String = default_version2, jobs: Int = default_jobs, component_name: String = "", verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current) { + Isabelle_System.require_command("git", "cmake") + Isabelle_System.with_tmp_dir("build")(tmp_dir => { /* component and platform */ val component = proper_string(component_name) getOrElse make_component_name(version1) val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) progress.echo("Component " + component_dir) val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) /* clone repository */ progress.echo("Cloning repository " + repository) progress.bash("git clone " + Bash.string(repository) + " vampire", cwd = tmp_dir.file, echo = verbose).check val source_dir = tmp_dir + Path.explode("vampire") File.copy(source_dir + Path.explode("LICENCE"), component_dir) /* build versions */ for { (rev, exe) <- List(version1 -> "vampire", version2 -> "vampire_polymorphic") } { progress.echo("Building " + exe + " (rev " + rev + ")") progress.bash("git checkout --quiet --detach " + Bash.string(rev), cwd = source_dir.file, echo = verbose).check val build_dir = source_dir + Path.explode("build") Isabelle_System.rm_tree(build_dir) Isabelle_System.make_directory(build_dir) val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else "" val cmake_out = progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" ..""", cwd = build_dir.file, echo = verbose).check.out val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r val binary = split_lines(cmake_out).collectFirst({ case Pattern(name) => name }) .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out)) progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check File.copy(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe, platform_dir + Path.basic(exe).platform_exe) } /* settings */ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64" ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire" ISABELLE_VAMPIRE_POLYMORPHIC="$VAMPIRE_HOME/vampire_polymorphic" VAMPIRE_EXTRA_OPTIONS="" """) /* README */ File.write(component_dir + Path.basic("README"), "This Isabelle component provides two versions of Vampire from\n" + repository + """ * vampire: standard version (regular stable release) * vampire_polymorphic: special version for polymorphic FOL and HOL (intermediate repository version) The executables have been built like this: git checkout COMMIT cmake . make The precise commit id is revealed by executing "vampire --version". Makarius """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_vampire", "build prover component from repository", Scala_Project.here, args => { var target_dir = Path.current var repository = default_repository var version1 = default_version1 var version2 = default_version2 var jobs = default_jobs var component_name = "" var verbose = false val getopts = Getopts(""" Usage: isabelle build_vampire [OPTIONS] Options are: -D DIR target directory (default ".") -U URL repository (default: """" + default_repository + """") -V REV1 standard version (default: """" + default_version1 + """") -W REV2 polymorphic version (default: """" + default_version2 + """") -j NUMBER parallel jobs for make (default: """ + default_jobs + """) -n NAME component name (default: """" + make_component_name("REV1") + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => repository = arg), "V:" -> (arg => version1 = arg), "W:" -> (arg => version2 = arg), "j:" -> (arg => jobs = Value.Nat.parse(arg)), "n:" -> (arg => component_name = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_vampire(repository = repository, version1 = version1, version2 = version2, component_name = component_name, jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_zipperposition.scala b/src/Pure/Admin/build_zipperposition.scala --- a/src/Pure/Admin/build_zipperposition.scala +++ b/src/Pure/Admin/build_zipperposition.scala @@ -1,121 +1,123 @@ /* Title: Pure/Admin/build_zipperposition.scala Author: Makarius Build Isabelle Zipperposition component from OPAM repository. */ package isabelle object Build_Zipperposition { - val default_version = "1.6" + val default_version = "2.0" /* build Zipperposition */ def build_zipperposition( version: String = default_version, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current) { Isabelle_System.with_tmp_dir("build")(build_dir => { - Isabelle_System.require_command("patchelf") + if (!Platform.is_windows) Isabelle_System.require_command("patchelf") /* component */ val component_name = "zipperposition-" + version val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) progress.echo("Component " + component_dir) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) /* build */ progress.echo("OCaml/OPAM setup ...") progress.bash("isabelle ocaml_setup", echo = verbose).check progress.echo("Building Zipperposition for " + platform_name + " ...") progress.bash(cwd = build_dir.file, echo = verbose, script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) + " zipperposition=" + Bash.string(version)).check /* install */ File.copy(build_dir + Path.explode("doc/zipperposition/LICENSE"), component_dir) val prg_path = Path.basic("zipperposition") val exe_path = prg_path.platform_exe File.copy(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path) - Executable.libraries_closure( - platform_dir + exe_path, filter = Set("libgmp"), patchelf = true) + if (!Platform.is_windows) { + Executable.libraries_closure( + platform_dir + exe_path, filter = Set("libgmp"), patchelf = true) + } /* settings */ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: ISABELLE_ZIPPERPOSITION="$COMPONENT/$ISABELLE_PLATFORM64/zipperposition" """) /* README */ File.write(component_dir + Path.basic("README"), """This is Zipperposition """ + version + """ from the OCaml/OPAM repository. Makarius """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository", Scala_Project.here, args => { var target_dir = Path.current var version = default_version var verbose = false val getopts = Getopts(""" Usage: isabelle build_zipperposition [OPTIONS] Options are: -D DIR target directory (default ".") -V VERSION version (default: """" + default_version + """") -v verbose Build prover component from OPAM repository. """, "D:" -> (arg => target_dir = Path.explode(arg)), "V:" -> (arg => version = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_zipperposition(version = version, verbose = verbose, progress = progress, target_dir = target_dir) }) }