diff options
| -rw-r--r-- | gnu/local.mk | 3 | ||||
| -rw-r--r-- | gnu/packages/java.scm | 132 | ||||
| -rw-r--r-- | gnu/packages/patches/tla2tools-build-xml.patch | 109 |
3 files changed, 243 insertions, 1 deletions
diff --git a/gnu/local.mk b/gnu/local.mk index 72bc31588d..37166bb2fc 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -1,5 +1,5 @@ # GNU Guix --- Functional package management for GNU -# Copyright © 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020 Ludovic Courtès <ludo@gnu.org> +# Copyright © 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2021 Ludovic Courtès <ludo@gnu.org> # Copyright © 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020 Andreas Enge <andreas@enge.fr> # Copyright © 2016 Mathieu Lirzin <mthl@gnu.org> # Copyright © 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021 Mark H Weaver <mhw@netris.org> @@ -1734,6 +1734,7 @@ dist_patch_DATA = \ %D%/packages/patches/tipp10-remove-license-code.patch \ %D%/packages/patches/tipp10-qt5.patch \ %D%/packages/patches/tk-find-library.patch \ + %D%/packages/patches/tla2tools-build-xml.patch \ %D%/packages/patches/transcode-ffmpeg.patch \ %D%/packages/patches/transmission-honor-localedir.patch \ %D%/packages/patches/ttf2eot-cstddef.patch \ diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm index d73f1acbf8..a167aafc38 100644 --- a/gnu/packages/java.scm +++ b/gnu/packages/java.scm @@ -14066,3 +14066,135 @@ can be interpreted by IDEs and static analysis tools to improve code analysis.") ;; either lgpl or asl license:lgpl3+ license:asl2.0)))) + +(define-public tla2tools + (let* ((version "1.8.0") + (tag (string-append "v" version))) + (package + (name "tla2tools") + (version version) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/tlaplus/tlaplus") + (commit tag))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1hhx8gmn81k8qrkx4p7ppinmygxga9fqffd626wkvhjgg2ky8lhs")) + (patches + (search-patches "tla2tools-build-xml.patch")) + (modules '((guix build utils))) + (snippet + '(begin + ;; Remove packaged libraries (see 'replace-libs below) + (for-each delete-file (find-files "." ".*.jar$")))))) + (build-system ant-build-system) + (arguments + (let* ((tlatools "tlatools/org.lamport.tlatools/") + (build-xml (string-append tlatools "customBuild.xml"))) + `(#:jdk ,openjdk11 + #:modules ((guix build ant-build-system) + (guix build utils) + (ice-9 match) + (srfi srfi-26)) + #:make-flags '("-f" ,build-xml) + #:phases + (modify-phases %standard-phases + ;; Replace packed libs with references to jars in store + (add-after 'unpack 'replace-libs + (lambda* (#:key inputs #:allow-other-keys) + (define (input-jar input) + (car (find-files (assoc-ref inputs input) "\\.jar$"))) + (for-each + (match-lambda + ((file . input) + (symlink (input-jar input) + (string-append ,tlatools "/lib/" file)))) + '(("gson/gson-2.8.6.jar" . "java-gson") + ("javax.mail/mailapi-1.6.3.jar" . "java-javax-mail") + ("jline/jline-terminal-3.14.1.jar" . "java-jline-terminal") + ("jline/jline-reader-3.14.1.jar" . "java-jline-reader") + ("lsp/org.eclipse.lsp4j.debug-0.10.0.jar" . + "java-eclipse-lsp4j-debug") + ("lsp/org.eclipse.lsp4j.jsonrpc-0.10.0.jar" . + "java-eclipse-lsp4j-jsonrpc") + ("lsp/org.eclipse.lsp4j.jsonrpc.debug-0.10.0.jar" . + "java-eclipse-lsp4j-jsonrpc-debug") + ("junit-4.12.jar" . "java-junit") + ("easymock-3.3.1.jar" . "java-easymock"))) + ;; Retain a tiny subset of the original X-Git-* + ;; manifest values just to aid in debugging + (substitute* ,build-xml + (("\\$\\{git.tag\\}") ,tag)))) + (add-before 'check 'prepare-tests + (lambda _ + ;; pcal tests write to cfg files + (for-each (cut chmod <> #o644) + (find-files (string-append ,tlatools + "/test-model/pcal") + "\\.cfg$")))) + (replace 'install + (lambda* (#:key inputs #:allow-other-keys) + (let* ((share (string-append %output "/share/java")) + (jar-name "tla2tools.jar"); set in project.properties + (jar (string-append ,tlatools + "/dist/" jar-name)) + (java-cp (string-append share "/" jar-name)) + (bin (string-append %output "/bin")) + (java (string-append (assoc-ref inputs "jdk") + "/bin/java"))) + (install-file jar share) + (mkdir-p bin) + ;; Generate wrapper scripts for bin/, which invoke common + ;; commands within tla2tools.jar. Users can still invoke + ;; tla2tools.jar for the rest. + (for-each + (match-lambda + ((wrapper . class) + (let ((file (string-append bin "/" wrapper))) + (begin + (with-output-to-file file + (lambda _ + (display + (string-append + "#!/bin/sh\n" + java " -cp " java-cp " " class " \"$@\"")))) + (chmod file #o755))))) + ;; bin/wrapper . java-class + '(("pcal" . "pcal.trans") + ("tlatex" . "tla2tex.TLA") + ("tla2sany" . "tla2sany.SANY") + ("tlc2" . "tlc2.TLC") + ("tlc2-repl" . "tlc2.REPL")))))))))) + (native-inputs + `(("java-junit" ,java-junit) + ("java-easymock" ,java-easymock))) + (inputs + `(("java-javax-mail" ,java-javax-mail) + ("java-gson" ,java-gson-2.8.6) + ("java-jline-terminal" ,java-jline-terminal) + ("java-jline-reader" ,java-jline-reader) + ("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc) + ("java-eclipse-lsp4j-jsonrpc-debug" ,java-eclipse-lsp4j-jsonrpc-debug) + ("java-eclipse-lsp4j-debug" ,java-eclipse-lsp4j-debug))) + (home-page "https://lamport.azurewebsites.net/tla/tools.html") + (synopsis "TLA+ tools (analyzer, TLC, TLATeX, PlusCal translator)") + (description "TLA+ is a high-level language for modeling programs and +systems---especially concurrent and distributed ones. It's based on the idea +that the best way to describe things precisely is with simple +mathematics. TLA+ and its tools are useful for eliminating fundamental design +errors, which are hard to find and expensive to correct in code. + +The following TLA+ tools are available in this distribution: + +@itemize +@item The Syntactic Analyzer: A parser and syntax checker for + TLA+ specifications; +@item TLC: A model checker and simulator for a subclass of \"executable\" TLA+ + specifications; +@item TLATeX: A program for typesetting TLA+ specifications; +@item Beta test versions of 1-3 for the TLA+2 language; and +@item The PlusCal translator. +@end itemize") + (license license:expat)))) diff --git a/gnu/packages/patches/tla2tools-build-xml.patch b/gnu/packages/patches/tla2tools-build-xml.patch new file mode 100644 index 0000000000..0bba82072a --- /dev/null +++ b/gnu/packages/patches/tla2tools-build-xml.patch @@ -0,0 +1,109 @@ +tla2tools comes packaged with three separate javax.mail JARs, which it +expects to be available to include in the JAR produced by the `dist' target. +However, the `java-javax-mail' packaged with Guix contains all of these +dependencies in a single JAR, so the other two are unneeded. This patch +removes references to them. + +The JAR also was expected to contain classes that are built as part of the +test suite. That does not seem useful, nor is it available during the +`compile' phase, so that portion is removed. + +There are a number of Git attributes that are set in the final manifest. +The branch name is kept, but the others are removed. The build user is set +statically to "guix". + +Finally, since we already have a patch, two targets `jar' and `check' are +added to satisfy `ant-build-system' and keep the package definition more +lean. + +diff --git a/tlatools/org.lamport.tlatools/customBuild.xml b/tlatools/org.lamport.tlatools/customBuild.xml +index f0ba77cb7..748e60d95 100644 +--- a/tlatools/org.lamport.tlatools/customBuild.xml ++++ b/tlatools/org.lamport.tlatools/customBuild.xml +@@ -36,6 +36,17 @@ + <istrue value="${maven.test.halt}"/> + </condition> + ++ <!-- `jar' and `check' added for Guix --> ++ <target name="jar"> ++ <antcall target="compile" inheritall="true" inheritrefs="true" /> ++ <antcall target="compile-aj" inheritall="true" inheritrefs="true" /> ++ <antcall target="dist" inheritall="true" inheritrefs="true" /> ++ </target> ++ <target name="check"> ++ <antcall target="compile-test" inheritall="true" inheritrefs="true" /> ++ <antcall target="test" inheritall="true" inheritrefs="true" /> ++ </target> ++ + <!-- https://github.com/alx3apps/jgit-buildnumber --> + <target name="git-revision"> + <taskdef name="jgit-buildnumber" classname="ru.concerteza.util.buildnumber.JGitBuildNumberAntTask"> +@@ -217,17 +228,7 @@ + <exclude name="javax/mail/search/**"/> + </patternset> + </unzip> +- <unzip src="lib/javax.mail/smtp-1.6.3.jar" dest="${class.dir}"> +- <patternset> +- <include name="**/*.class"/> +- </patternset> +- </unzip> +- <unzip src="lib/javax.mail/javax.activation_1.1.0.v201211130549.jar" dest="${class.dir}"> +- <patternset> +- <include name="**/*.class"/> +- <exclude name="org/**"/> +- </patternset> +- </unzip> ++ <mkdir dir="${class.dir}/META-INF" /> + <touch file="${class.dir}/META-INF/javamail.default.address.map"/> + <unzip src="lib/jline/jline-terminal-3.14.1.jar" dest="${class.dir}"> + <patternset> +@@ -259,17 +260,7 @@ + <exclude name="javax/mail/search/**"/> + </patternset> + </unzip> +- <unzip src="lib/javax.mail/smtp-1.6.3.jar" dest="target/classes"> +- <patternset> +- <include name="**/*.class"/> +- </patternset> +- </unzip> +- <unzip src="lib/javax.mail/javax.activation_1.1.0.v201211130549.jar" dest="target/classes"> +- <patternset> +- <include name="**/*.class"/> +- <exclude name="org/**"/> +- </patternset> +- </unzip> ++ <mkdir dir="target/classes/META-INF" /> + <touch file="target/classes/META-INF/javamail.default.address.map"/> + + <unzip src="lib/jline/jline-terminal-3.14.1.jar" dest="target/classes"> +@@ -373,14 +364,8 @@ + src/tla2sany/parser/Token.09-09-07, + src/tla2sany/parser/TokenMgrError.09-09-07"/> + <fileset dir="${doc.dir}" includes="License.txt"/> +- <fileset dir="${test.class.dir}"> +- <include name="**/tlc2/tool/CommonTestCase*.class" /> +- <include name="**/tlc2/tool/liveness/ModelCheckerTestCase*.class" /> +- <include name="**/tlc2/TestMPRecorder*.class" /> +- <include name="**/util/IsolatedTestCaseRunner*.class" /> +- </fileset> + <manifest> +- <attribute name="Built-By" value="${user.name}" /> ++ <attribute name="Built-By" value="guix" /> + <attribute name="Build-Tag" value="${env.BUILD_TAG}" /> + <attribute name="Build-Rev" value="${Build-Rev}" /> + <attribute name="Implementation-Title" value="TLA+ Tools" /> +@@ -389,14 +374,8 @@ + <!-- The jar files contains many main classes (SANY, TEX, pcal, ...) --> + <!-- but lets consider TLC the one users primarily use. --> + <attribute name="Main-class" value="tlc2.TLC" /> +- <attribute name="Class-Path" value="CommunityModules-deps.jar CommunityModules.jar" /> + <!-- Git revision --> +- <attribute name="X-Git-Branch" value="${git.branch}" /> + <attribute name="X-Git-Tag" value="${git.tag}" /> +- <attribute name="X-Git-Revision" value="${git.revision}" /> +- <attribute name="X-Git-ShortRevision" value="${git.shortRevision}" /> +- <attribute name="X-Git-BuildNumber" value="${git.branch}_${git.tag}_${git.shortRevision}" /> +- <attribute name="X-Git-Commits-Count" value="${git.commitsCount}" /> + <!-- App-Name and Permissions is required by Java Webstart used by distributed TLC --> + <!-- Depending on security level, the user will see a warning otherwise. --> + <!-- http://docs.oracle.com/javase/7/docs/technotes/guides/jweb/security/manifest.html --> |