diff options
Diffstat (limited to 'dev-lang/dafny')
-rw-r--r-- | dev-lang/dafny/Manifest | 4 | ||||
-rw-r--r-- | dev-lang/dafny/dafny-4.4.0-r1.ebuild (renamed from dev-lang/dafny/dafny-4.4.0.ebuild) | 56 | ||||
-rw-r--r-- | dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch | 21 | ||||
-rw-r--r-- | dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch | 18 |
4 files changed, 46 insertions, 53 deletions
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest index 018f7181ec1f..e8e4e4b4a3d7 100644 --- a/dev-lang/dafny/Manifest +++ b/dev-lang/dafny/Manifest @@ -5,8 +5,6 @@ AUX dafny-4.2.0-lit-use-system-boogie.patch 531 BLAKE2B a9b37e00fcbd204e525caecd AUX dafny-4.3.0-net6.0-upgrade.patch 949 BLAKE2B 3ea7a94a6786193c35228ed721140b1304b706ae14398e718d55a7d1a6469af63534b82d24ed52c34e12996d89ef196472b322c10fdeef16fd922cd17f920734 SHA512 f5fb2dcb40078038b26525e986004612c6d161904ffb3379d15e4c4082a1d9e04218ab4a6800e095e11636f1b0f2743415b91fb2b0ce9ec1aa797257782e103c AUX dafny-4.4.0-lit-config.patch 421 BLAKE2B 70c442fd505fbe350e31212ee23746d2b43c8f713de004a8ea0c801d46be5bf98f7a2feddad94ed91661621003ae6d20c10e57b3c8a7ecd8699a012507535740 SHA512 9c010d990ebfc6ba046c61489a138f4047ed7e17121f093fac19bee274baa40fc1fbff11d6f637aaf93e55de69c30709b53291fd3991adf9938d811f6c1f9599 AUX dafny-4.4.0-lit-system-boogie.patch 623 BLAKE2B e10f224ad87ce64af785b8f2409395d69824c921be51b6271c2c1beaf3d2020a293dadd5b2735aed32d25737431bd6d4307ac7ee28cfd3753393ac262d88395c SHA512 97e06ec2ad1f1086aeb8726f90a0316ff1d1ccfd6aaaeadd00f913d79c5e88abaa7f6ea7899a0f37ae521ad27f674bb4cbce9b7f25a1b5ee462c06adf594d146 -AUX dafny-4.4.0-no-copy-jar.patch 885 BLAKE2B 898da1cef1d53532cf7426a46877ce17f1351d76ec73c5c1482de1dbc9c5241fe1c952c7eacd565a639261a2ecf61132eae38a04cd794c4178acf0d365195163 SHA512 11c0bf2088b7fae2ec714b5ead4cfc9381a51a8946d32ae33147fba54072c275b6775195cc16bf1c232fc1b5799317c72d785de4097cd9dc9340e6ff2fffe28c -AUX dafny-4.4.0-no-output-jar.patch 987 BLAKE2B d75565200cdd120def48af780e6b11d0ae8f5e9f1192ad6c4930d807f982fea235dc9a50502c68eaf4c55529465a972e2442efd3ec8fd1947bbd295d643a518d SHA512 10e421ccfaed82f756219003d046605595974d4359aa58085a9d7affedc921b506432af05acc11bd918d322f363724ab850a8e8fa2714bf9bbcd86f99b3955ce DIST bignumber.js-9.1.2.tgz 79226 BLAKE2B 3d2ff19d73a6fcfbcc0d03d1e9808796baae639e19973cbe0c26af4b514abc299129b8a7bc3e4e803c61af44b76f4381b1965d8fa331ea43e8a4c8fc7f98d8e7 SHA512 dbf98ac991fd2bce5bcce11f8570c11594c6775093b3ee481e9785428f65ba2046ee1821742f39d4f8f658085be84dd1e9bf6d663fd72a16e0e1fba6f8a7a9ba DIST boogie.abstractinterpretation.2.16.8.nupkg 29244 BLAKE2B 0e8deed122c8109b145bd2fe8f4134dbb9dfac1b934081b45e5ce89ce9147d47e6b26f6408fe47a9fb3228f8eaf783e289062991d07580d21b4092b36e6571e7 SHA512 04dcf0db58ced0f65ded090a7429bb213c9f45c7387ea0cf20f4c37ecd7630d03ead35e8029cd416296df6c5e9d2ca0cbd1c329b90fe96c19669cbf0be8828e6 DIST boogie.abstractinterpretation.3.0.9.nupkg 29646 BLAKE2B 20b0e150d3a9a6ed11a24cd9920a97971d515207d86864a9b1cd4d554b2b3c34e27778051a9bf6d8b3178352a6cfbb33c363b2d69958f6503e17e366ca3e1147 SHA512 26b75a409b4bfe5dd4ac982ca2c1b03df2118254a9becaab74f4d44b652746faa0448ab943ee9177f6a0fd105f8ce015a4403b6ff58df12201b542c50618b222 @@ -375,5 +373,5 @@ DIST xunit.runner.visualstudio.2.4.3.nupkg 809588 BLAKE2B ce18ac895657d1efa9752e DIST xunit.runner.visualstudio.2.5.1.nupkg 348549 BLAKE2B 530ffc6b699a1589ad6a7fb5aa826d7238b63ea8dcd13ce5705a3d29a0ba70edeac2d9950cd1a00a13a779add761e4e14335689051a43b4cd662a330734e4df7 SHA512 0cc7887e7c7c3315db31aab79df236db9b5542e0234c27543dd5b11cf917674a8fdebc384e7331663b08d586fcf20628479a20ad7edbed4e61667903e812c6f0 DIST xunit.skippablefact.1.4.8.nupkg 44542 BLAKE2B 3c9b09d5196e8901770099b2e5078d9373e8ebc2da058a9071707d6fee56eab7c876578734f3be5b088db6ae83c8ad81a3aadfcab38e1fd2b28bd25601fe5463 SHA512 a2c680223bda4f9bfdbd751c8d6a5319e0a4611533272860ca0a396b26c473a13065301a5d8973074ea2bb5119caaeec5a67d547a96ae5d762dc09f337f51ad1 EBUILD dafny-4.3.0-r1.ebuild 19287 BLAKE2B 3d9e22094a7fc2f6ec8117760a1d009cf338f42c2a81becdffcbb17a828207473a11e7cb42d4e5e8013629ef77473b691240bb9cc06a76b869a3114428189bd7 SHA512 854890a61314c76b55bc823f730979f9d06d4f67abb65012f4ad2d2fbdf826d5845a268a0239f33169c8d6aae34acadbe85877358cb9eaaf0fb796d93c79cc13 -EBUILD dafny-4.4.0.ebuild 17918 BLAKE2B 22c57059fccf1a6ff66563f9a8405bbb5240326d4cd0d694ae81785f8ab4dcd163308f31b9e4a5971062e075da3ebc852fdb1e9737b2821c8f689d991355cded SHA512 21e1f06dcfc025d8b6ed3da3ca91b4037498badc47e158a424f58bd603d88dbdb07916f863b076bb42caa61569aff4db657092041a808c7343592bc247a919a9 +EBUILD dafny-4.4.0-r1.ebuild 18792 BLAKE2B 358087074aaf1b24fd56f202a171baa06bd9b008a79b228b0b2b8d1268cec4c657934dbe1c65aede09d1d9717f60a7512dfe14052f720115fcf8e9c235543ec5 SHA512 3e59ae339b0795b08de1d6eb319ae79717628f1920b8d5c1d64f4760f18f681d2a978b5e6b875c304380d328c72485dcbd2e634ec781b1b531c7033bf1c286da MISC metadata.xml 1884 BLAKE2B e3a53cfd90a4edf1d9fd9f567ac3c23fd88cc46602cfe6aea31ddc40585ebc89ab82833dcd21c82083671a54454d62f162f45d56d6b0ec9c202148b3d5ea2c6d SHA512 4cffb9c237ed85097ce1496a72f5aa9c5a0f5758402fe66ff745a3b1dbc3f8d9a40fecc9140ee1b9418f09b62794f7e0a47f908e6ba01b370087d4df62bfa46e diff --git a/dev-lang/dafny/dafny-4.4.0.ebuild b/dev-lang/dafny/dafny-4.4.0-r1.ebuild index 50a6fd8da3c2..617b0a373ba8 100644 --- a/dev-lang/dafny/dafny-4.4.0.ebuild +++ b/dev-lang/dafny/dafny-4.4.0-r1.ebuild @@ -361,7 +361,7 @@ xunit@2.4.1 xunit@2.4.2 " -inherit check-reqs dotnet-pkg edo multiprocessing python-any-r1 +inherit check-reqs dotnet-pkg edo java-pkg-2 multiprocessing python-any-r1 DESCRIPTION="Dafny is a verification-aware programming language" HOMEPAGE="https://dafny.org/ @@ -390,8 +390,12 @@ RESTRICT="!test? ( test )" RDEPEND=" !dev-lang/dafny-bin + >=virtual/jre-1.8:* sci-mathematics/z3 " +DEPEND=" + >=virtual/jdk-1.8:* +" BDEPEND=" ${RDEPEND} dev-dotnet/coco @@ -416,8 +420,6 @@ PATCHES=( "${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch" "${FILESDIR}/${PN}-4.4.0-lit-config.patch" "${FILESDIR}/${PN}-4.4.0-lit-system-boogie.patch" - "${FILESDIR}/${PN}-4.4.0-no-copy-jar.patch" - "${FILESDIR}/${PN}-4.4.0-no-output-jar.patch" ) DOCS=( @@ -436,8 +438,15 @@ pkg_setup() { # Clean the environment. unset NPM_CONFIG_USERCONFIG + if [[ -n "${_JAVA_OPTIONS}" ]] ; then + ewarn "Cleaning _JAVA_OPTIONS because when set compile and test may fail" + + unset _JAVA_OPTIONS + fi + check-reqs_pkg_setup dotnet-pkg_pkg_setup + java-pkg-2_pkg_setup # We need to set up Python only for running test tools (called via lit). if use test ; then @@ -459,41 +468,52 @@ src_prepare() { if grep "// RUN: %testDafnyForEachCompiler" "${test_file}" >/dev/null ; then rm "${test_file}" || die fi - done < <(find "${TEST_S}" -type f -name "*.dfy") + done < <(find "${TEST_S}" -type f -name "*.dfy") # Remove bad tests (recursive). local -a bad_tests=( # Following tests fail: - DafnyTests/TestAttribute.dfy VSComp2010/Problem2-Invert.dfy auditor/TestAuditor.dfy benchmarks/sequence-race/SequenceRace.dfy - comp/CoverageReport.dfy dafny0/Fuel.legacy.dfy dafny0/JavaUseRuntimeLib.dfy dafny0/Stdin.dfy dafny4/Lucas-up.legacy.dfy - examples/Simple_compiler/Compiler.dfy git-issues/git-issue-2026.dfy git-issues/git-issue-2299.dfy git-issues/git-issue-2301.dfy - metatests/InconsistentCompilerBehavior.dfy - metatests/TestBeyondVerifierExpect.dfy separate-verification/assumptions.dfy server/counterexample_none.transcript - unicodechars/expectations/Expect.dfy wishlist/exists-b-exists-not-b.dfy # Following tests are very slow: + VSI-Benchmarks/b4.dfy + comp/CompileWithArguments.dfy + comp/MainMethod.dfy + comp/compile3/JustRun.dfy + concurrency/07-CounterThreadOwnership.dfy + concurrency/09-CounterNoStateMachine.dfy + concurrency/10-SequenceInvariant.dfy + concurrency/12-MutexLifetime-short.dfy + dafny1/SchorrWaite.dfy + dafny2/SnapshotableTrees.dfy + dafny4/git-issue250.dfy + git-issues/git-issue-Main4.dfy + git-issues/git-issue-MainE.dfy + unicodechars/comp/CompileWithArguments.dfy ) local bad_test for bad_test in "${bad_tests[@]}" ; do rm "${TEST_S}/${bad_test}" || die "failed to remove test ${bad_test}" done + dotnet-pkg_src_prepare + # Update lit's "lit.site.cfg" file. local dotnet_exec="${DOTNET_PKG_EXECUTABLE} exec ${DOTNET_PKG_OUTPUT}" local lit_config="${TEST_S}/lit.site.cfg" + sed "/^defaultDafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \ -i "${lit_config}" || die "failed to update ${lit_config}" sed "/^dafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \ @@ -506,8 +526,22 @@ src_prepare() { -i "${lit_config}" || die "failed to update ${lit_config}" sed "/^serverExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \ -i "${lit_config}" || die "failed to update ${lit_config}" +} - dotnet-pkg_src_prepare +src_compile () { + einfo "Building DafnyRuntimeJava JAR." + local dafny_runtime_java="${S}/Source/DafnyRuntime/DafnyRuntimeJava" + mkdir -p "${dafny_runtime_java}/build/libs/" || die + pushd "${dafny_runtime_java}/build" || die + + ejavac -d ./ $(find "${dafny_runtime_java}/src/main" -type f -name "*.java") + edo jar cvf "DafnyRuntime-${PV}.jar" dafny/* + + cp "DafnyRuntime-${PV}.jar" "${dafny_runtime_java}/build/libs/" || die + popd || die + + # Build main dotnet package. + dotnet-pkg_src_compile } src_test() { diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch deleted file mode 100644 index 96ab9fc4a723..000000000000 --- a/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch +++ /dev/null @@ -1,21 +0,0 @@ ---- a/Source/DafnyPipeline/DafnyPipeline.csproj -+++ b/Source/DafnyPipeline/DafnyPipeline.csproj -@@ -89,11 +89,6 @@ - <LinkBase>DafnyRuntimeJava</LinkBase>
- <CopyToOutputDirectory>Always</CopyToOutputDirectory>
- </EmbeddedResource>
-- <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.4.0.jar">
-- <LogicalName>DafnyRuntime.jar</LogicalName>
-- <Link>DafnyRuntime.jar</Link>
-- <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
-- </EmbeddedResource>
- <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntime.cs">
- <LinkBase>DafnyRuntimeCsharp</LinkBase>
- <CopyToOutputDirectory>Always</CopyToOutputDirectory>
-@@ -128,4 +123,4 @@ - <EmbeddedResource Remove="..\DafnyRuntime\DafnyRuntimeRust\target\**"/>
- </ItemGroup>
-
--</Project> -\ No newline at end of file -+</Project>
diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch deleted file mode 100644 index 332fc4ffb49f..000000000000 --- a/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch +++ /dev/null @@ -1,18 +0,0 @@ ---- a/Source/DafnyRuntime/DafnyRuntime.csproj -+++ b/Source/DafnyRuntime/DafnyRuntime.csproj -@@ -28,15 +28,5 @@ - <PropertyGroup>
- <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.4.0.jar</DafnyRuntimeJar>
- </PropertyGroup>
-- <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
--
-- <Message Text="Compiling DafnyRuntimeJava to $(DafnyRuntimeJar)..." Importance="high" />
-- <!-- For some reason the DafnyRuntime.jar was often not (yet?) created after this Target was run, leading to build failures.
-- We've removed the 'clean' step that was before 'build', so the DafnyRuntime.jar from a previous run can be used. -->
-- <ItemGroup>
-- <!-- Register the generated file to be deleted when cleaning -->
-- <FileWrites Include="$(DafnyRuntimeJar)" />
-- </ItemGroup>
-- </Target>
-
- </Project>
|