isabelle: 2025 -> 2025-1 (#474227) (fc399e25) · Commits · nix / nixpkgs

pkgs/by-name/is/isabelle/components/isabelle-linter.nix

+3 −3

Original line number	Diff line number	Diff line
		@@ -7,13 +7,13 @@

		stdenv.mkDerivation rec {
		pname = "isabelle-linter";
		version = "2025-1.0.0";
		version = "2025-1-1.0.0";

		src = fetchFromGitHub {
		owner = "isabelle-prover";
		repo = "isabelle-linter";
		rev = "Isabelle2025-v1.0.0";
		hash = "sha256-cH9EoIbKa6cqLjw83gnYvCy+Dq0d5fFmJCabdPrRJeI=";
		rev = "Isabelle2025-1-v1.0.0";
		hash = "sha256-4J1lEvBNlfZudEEqsU3zOUewKSC4xZ3HTZGwgJCf9kc=";
		};

		nativeBuildInputs = [ isabelle ];

pkgs/by-name/is/isabelle/package.nix

+44 −11

Original line number	Diff line number	Diff line
		@@ -3,9 +3,10 @@
		stdenv,
		fetchurl,
		fetchFromGitHub,
		gcc14Stdenv,
		coreutils,
		net-tools,
		java,
		openjdk21,
		scala_3,
		polyml,
		verit,
		@@ -21,13 +22,43 @@
		}:

		let
		vampire' = vampire.overrideAttrs (_: {
		java = openjdk21;

		# There have been issues with proofs failing on NixOS in the past,
		# so we pin polyml to the exact commit that upstream isabelle uses
		polyml' = polyml.overrideAttrs {
		pname = "polyml-for-isabelle";
		version = "2025-1";

		src = fetchFromGitHub {
		owner = "polyml";
		repo = "polyml";
		rev = "ccd3e3717f7238b9b5d295fea4b5426182dfc0b6";
		hash = "sha256-wYW8aSvXzhW3hCDeorkD59j+1S6smzsFXHuPYeqo7z8=";
		};

		configureFlags = [
		"--enable-intinf-as-int"
		"--with-gmp"
		"--disable-shared"
		];
		buildFlags = [ "compiler" ];
		};

		# Isabelle uses a branch of vampire that is not in the normal release line
		# that adds support for higher order goals
		vampire' = (vampire.override { stdenv = gcc14Stdenv; }).overrideAttrs (_: {
		pname = "vampire-for-isabelle";
		version = "4.8";

		src = fetchFromGitHub {
		owner = "vprover";
		repo = "vampire";
		tag = "v4.8HO4Sledgahammer";
		hash = "sha256-CmppaGa4M9tkE1b25cY1LSPFygJy5yV4kpHKbPqvcVE=";
		};

		cmakeFlags = [ (lib.cmakeFeature "CMAKE_BUILD_HOL" "On") ];
		});

		sha1 = stdenv.mkDerivation {
		@@ -56,7 +87,7 @@ let
		in
		stdenv.mkDerivation (finalAttrs: {
		pname = "isabelle";
		version = "2025";
		version = "2025-1";

		dirname = "Isabelle${finalAttrs.version}";

		@@ -64,23 +95,23 @@ stdenv.mkDerivation (finalAttrs: {
		if stdenv.hostPlatform.isDarwin then
		fetchurl {
		url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_macos.tar.gz";
		hash = "sha256-6ldUwiiFf12dOuJU7JgUeX8kU+opDfILL23LLvDi5/g=";
		hash = "sha256-WKlrsXP6oZHy6NTaaQYpddtgE2QGhBZ4uKai61dtQ14=";
		}
		else if stdenv.hostPlatform.isx86 then
		fetchurl {
		url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_linux.tar.gz";
		hash = "sha256-PR1m3jcYI/4xqormZjj3NXW6wkTwCzGu4dy2LzgUfFY=";
		hash = "sha256-0SA28X3fIKMV3wZtlJvBxq9MZkI6GevVuSNzgqJ4xQU=";
		}
		else
		fetchurl {
		url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_linux_arm.tar.gz";
		hash = "sha256-p/Hp+7J5gJy5s6BVD5Ma1Mu2OS53I8BS7gKSOYYB0PE=";
		hash = "sha256-BUhdK8qhdV2Den+4bbdd9T6MD/BtGpxp+1Axj21NxrI=";
		};

		nativeBuildInputs = [ java ];

		buildInputs = [
		polyml
		polyml'
		verit
		vampire'
		eprover-ho
		@@ -102,6 +133,9 @@ stdenv.mkDerivation (finalAttrs: {
		postPatch = ''
		patchShebangs lib/Tools/ bin/

		substituteInPlace src/Pure/ML/ml_settings.scala \
		--replace-fail 'polyml_home + Path.basic(ml_platform)' 'Path.explode("${polyml'}/bin")'

		cat >contrib/verit-*/etc/settings <<EOF
		ISABELLE_VERIT=${verit}/bin/veriT
		EOF
		@@ -119,9 +153,8 @@ stdenv.mkDerivation (finalAttrs: {

		cat >contrib/polyml-*/etc/settings <<EOF
		ML_SYSTEM_64=true
		ML_SYSTEM=${polyml.name}
		ML_SYSTEM=${polyml'.name}
		ML_PLATFORM=${stdenv.system}
		ML_HOME=${polyml}/bin
		ML_OPTIONS="--minheap 1000"
		POLYML_HOME="\$COMPONENT"
		ML_SOURCES="\$POLYML_HOME/src"
		@@ -192,11 +225,12 @@ stdenv.mkDerivation (finalAttrs: {
		ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"
		done
		echo "Building isabelle setup"
		javac -d "$TARGET_DIR" -classpath "${scala_3.bare}/lib/scala3-interfaces-${scala_3.version}.jar:${scala_3.bare}/lib/scala3-compiler_3-${scala_3.version}.jar" "''${ARGS[@]}"
		javac -d "$TARGET_DIR" -classpath "${scala_3.bare}/lib/scala3-interfaces-${scala_3.version}.jar:${scala_3.bare}/lib/scala3-compiler_3-${scala_3.version}.jar:./contrib/flatlaf-3.6.2/lib/flatlaf-3.6.2-no-natives.jar" "''${ARGS[@]}"
		jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle
		rm -rf "$TARGET_DIR/isabelle"

		echo "Building HOL heap"
		ln -s ${polyml'}/bin ./contrib/polyml-*/
		bin/isabelle build -v -o system_heaps -b HOL
		'';

		@@ -243,7 +277,6 @@ stdenv.mkDerivation (finalAttrs: {
		];
		license = lib.licenses.bsd3;
		maintainers = [
		lib.maintainers.jwiegley
		lib.maintainers.jvanbruegge
		];
		platforms = lib.platforms.unix;

pkgs/top-level/all-packages.nix

+0 −15

Original line number	Diff line number	Diff line
		@@ -13206,21 +13206,6 @@ with pkgs;

		inherit (ocamlPackages) hol_light;

		isabelle = callPackage ../by-name/is/isabelle/package.nix {
		polyml = polyml.overrideAttrs {
		pname = "polyml-for-isabelle";
		version = "2025";
		__intentionallyOverridingVersion = true; # avoid a warning, no src override
		configureFlags = [
		"--enable-intinf-as-int"
		"--with-gmp"
		"--disable-shared"
		];
		buildFlags = [ "compiler" ];
		};

		java = openjdk21;
		};
		isabelle-components = recurseIntoAttrs (callPackage ../by-name/is/isabelle/components { });

		lean3 = lean;

Admin message