18/18: gnu: Add tla2tools.

[guix-commits]

civodul pushed a commit to branch master
in repository guix.

commit f30e8f29096e3ae2a4de689690daf5fa27a8c91b
Author: Mike Gerwitz <mtg@gnu.org>
AuthorDate: Thu Apr 15 21:24:39 2021 -0400

    gnu: Add tla2tools.
    
    This introduces tla2tools.jar, which contains the TLA+ model checker
    and simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeX
    typesetting system; PlusCal translator; and more.  I have added five
    wrapper scripts for convenience, rather than invoking `java' manually.
    The wrapper scripts are not comprehensive; users who are familiar with
    tla2tools.jar, or have read the book Specifying Systems, may still
    invoke the commands in the traditional way.
    
    The minimum JDK version is 11.  I chose to stick with that rather than
    bumping it to 14 (which is the largest version currently in Guix)
    because each OpenJDK version in Guix depends on the version before it,
    and so it needlessly results in many 100s of MiB of unnecessary
    dependencies.
    
    Note that this is _not_ the TLA+ Toolbox, which is the GUI commonly used
    with TLA+.
    
    * gnu/packages/java.scm (tla2tools): New variable.
    * gnu/packages/patches/tla2tools-build-xml.patch: New patch.
    * gnu/local.mk (dist_patch_DATA): Add it.
    
    Signed-off-by: Ludovic Courtès <ludo@gnu.org>
---
 gnu/local.mk                                   |   3 +-
 gnu/packages/java.scm                          | 132 +++++++++++++++++++++++++
 gnu/packages/patches/tla2tools-build-xml.patch | 109 ++++++++++++++++++++
 3 files changed, 243 insertions(+), 1 deletion(-)

diff --git a/gnu/local.mk b/gnu/local.mk
index 72bc315..37166bb 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 d73f1ac..a167aaf 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 0000000..0bba820
--- /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
 -->