[PATCH 0/6] Add TLA+ Tools (tla2tools)

  • Done
  • quality assurance status badge
Details
4 participants
  • Julien Lepiller
  • Ludovic Courtès
  • Maxime Devos
  • Mike Gerwitz
Owner
unassigned
Submitted by
Mike Gerwitz
Severity
normal
M
M
Mike Gerwitz wrote on 15 Apr 2021 06:22
(address . guix-patches@gnu.org)
cover.1618460450.git.mtg@gnu.org
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.

This was significnatly more involved than I had anticipated, and I was
forced to make some compromises on how I handled dependencies. Most
notably, rather than packaging the entirety of LSP4J and JLine 3, I packaged
only what tla2tools used, since going all the way would have been a
significant undertaking that I would not have been able to see through.

I have not packaged Java libraries for Guix before (and it's been years
since I packaged anything else), so please be critical and let me know what
I can do better.

I hope to explore packaging TLAPS next. I don't anticipate packaging the
Toolbox for Guix, which is TLA+'s GUI; there are a huge number of
dependencies.

Enjoy!

Mike Gerwitz (6):
gnu: Add java-gson-2.8.6.
gnu: Add java-eclipse-xtext-xbase-lib.
gnu: Add java-eclipse-lsp4j packages.
gnu: Add java-jline-terminal.
gnu: Add java-jline-reader.
gnu: Add tla2tools.

gnu/packages/java.scm | 410 ++++++++++++++++++
.../patches/tla2tools-build-xml.patch | 109 +++++
2 files changed, 519 insertions(+)
create mode 100644 gnu/packages/patches/tla2tools-build-xml.patch

--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3v24ACgkQjJF7f13F
G6JLtBAAjHMEfjqhCSaFk04meRrVvzE//XJOYfFyMpsqvASO354rKX/H3FT1iRuE
585wcjv7DCsYruv+mTU9/eNYXgti8Q4e8l07PornvjXtMswi1R+XyqbbEmqHT8lJ
mhn4NsZ66zPHccd51jqraes5RX618sjWg7hj4BTc5bgB/DktLL5OBJnQFiVIk2/9
O623zKiRCxjgWE2nUe4uwc52rlzKrR/8eSL4VlV5cE4VISrR1cd25toIr1pCgsbB
CUkFP77oc+Tb2MRzrQ0nABfQe7yYoFwVrEwEfDWs2yQoJKxMYLJ+E37JMjdgEGwQ
841wmOeJA1w5s5JP5twpMBBc0UX2F7PRM50F8+uXblMBW+/Ca+HCZLvRY3MnQNo6
YQ3JCiUXiPtfeMufpmyLOcymFsnfGhodw50kdZ8BCNShESW9viEbQtk8H9auQZfF
e9t4cvafdg9NCaFfQp2wF+b1fTGtiiO5IzFWJeBTFsYbymGKFsIX3qV4vtZH/2OC
f8jE1Gd3lzZxybvykUszRrsDkO78diNgN1CnOVE6TtpVJ90ggGo50UJEIRK5dQJ9
ulYJNNMx3M2KYzjnjKfdVGFRes7cDxzkF4CIxbyLiGORTj7AytNmrTBOdQlcbQ0j
CattBrFFZn6tV2Jf3BNchUMCrBPz0CpB4sNo6BRuVh1sjzVtagQ=
=M6PH
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:25
[PATCH 1/6] gnu: Add java-gson-2.8.6.
(address . 47789@debbugs.gnu.org)
0bb3e905602bcba367d14ad4ff20ef3caa54f72b.1618460450.git.mtg@gnu.org
This introduces a new package rather than upgrading the exist java-gson
package because it is built using OpenJDK11; I didn't want to have to
propagate that JDK dependency to the other packages that use it.

OpenJDK 11 was chosen becuase this dependency was introduced for
tla2tools.

* gnu/packages/java.scm (java-gson-2.8.6): New variable.
---
gnu/packages/java.scm | 43 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 43 insertions(+)

Toggle diff (66 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 207f136513..fe75404e9c 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -15,6 +15,7 @@
;;; Copyright © 2020 Raghav Gururajan <raghavgururajan@disroot.org>
;;; Copyright © 2020 Maxim Cournoyer <maxim.cournoyer@gmail.com>
;;; Copyright © 2021 Vincent Legoll <vincent.legoll@gmail.com>
+;;; Copyright © 2021 Mike Gerwitz <mtg@gnu.org>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -11724,6 +11725,48 @@ string to an equivalent Java object. Gson can work with arbitrary Java objects
including pre-existing objects that you do not have source-code of.")
(license license:asl2.0)))
+;; This requires a different Java version than 2.8.2 above
+(define-public java-gson-2.8.6
+ (package
+ (name "java-gson")
+ (version "2.8.6")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/google/gson")
+ (commit (string-append "gson-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0kk5p3vichdb0ph1lzknrcpbklgnmq455mngmjpxvvj29p3rgpk3"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "gson.jar"
+ #:jdk ,openjdk11
+ #:source-dir "gson/src/main/java"
+ #:test-dir "gson/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ ;; avoid Maven dependency
+ (add-before 'build 'fill-template
+ (lambda _
+ (with-directory-excursion "gson/src/main"
+ (copy-file "java-templates/com/google/gson/internal/GsonBuildConfig.java"
+ "java/com/google/gson/internal/GsonBuildConfig.java")
+ (substitute* "java/com/google/gson/internal/GsonBuildConfig.java"
+ (("\\$\\{project.version\\}") ,version)))
+ #t)))))
+ (native-inputs
+ `(("java-junit" ,java-junit)
+ ("java-hamcrest-core" ,java-hamcrest-core)))
+ (home-page "https://github.com/google/gson")
+ (synopsis "Java serialization/deserialization library from/to JSON")
+ (description "Gson is a Java library that can be used to convert Java
+Objects into their JSON representation. It can also be used to convert a JSON
+string to an equivalent Java object. Gson can work with arbitrary Java objects
+including pre-existing objects that you do not have source-code of.")
+ (license license:asl2.0)))
+
(define-public java-hawtjni
(package
(name "java-hawtjni")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wCgACgkQjJF7f13F
G6KmKA/+OS2SnWXIdcRLvPzy0C2fJxdCVRN76GJy5i3g9OU0ZrEBOtdGGBdnt9wL
jSkuOb+9dnGz198B+g6bZAJ0/w+0SvaSUF7m1iD0scOc52KbWQ1MFxtZYUICJ5K9
ow+Hfi9+ldMujgXNFaAzxKhyEbHiGVBlucDLGiXmvRMAUTICSkCGIC6AyEloM2Bh
82M5K+/fMFR9oX1tkYn9H9rsvoq1TVxGaAvYzcss+aj/VttvmQPPfW9fd/ubyAZc
TtOioybWTz65/5RouZSTsUcOyE5A/A0s78f408XJ6KlJvndmR8JUgnecbneHLteJ
Bea0Sntn62MV3YxxCyBYR33Q00l+WyFhT97NADFJg4f/Ig7JGdxOz3/tflHh3XQI
nzf9L/4Ci6y608oXYS5C562RMgzLwg9SWZaj++KBWkV5sXNUkP0DTZyYzt1o6hMY
DS0EG/Z8G6iCh9bKum71EE7D5BdVqcZJPjTd8cZjYG454DstiTF6LqGSamAcHfeo
AjQyLVkSrJFNi+kFxmaMOJo5QsHnsMLFs09RCiC/x/UEq70WEbsrwP3wazsg5NtN
72Jvyo6EjHzRbMpPJMkkqqtUFiuPM6HK9k2StHeqT68PFr0YMC6oy0VM9ZsD+Gyh
jkA6D7I4UTxiw9DiFUq5HaGLziXsaqeN9fH7PglCNjgf557tOJs=
=1Mmw
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:26
[PATCH 2/6] gnu: Add java-eclipse-xtext-xbase-lib.
(address . 47789@debbugs.gnu.org)
294c4acfdf0598ebebeece871be847b4058d84a0.1618460450.git.mtg@gnu.org
This package is a component of xtext-lib. The rest of xtext-lib was not
added.

* gnu/packages/java.scm (java-eclipse-xtext-xbase-lib): New variable.
---
gnu/packages/java.scm | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)

Toggle diff (46 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index fe75404e9c..b0e67b2f6e 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -7547,6 +7547,36 @@ means for generating files and compiling new Java classes based on annotations
found in your source code.")
(license license:epl2.0)))
+(define-public java-eclipse-xtext-xbase-lib
+ (package
+ (name "java-eclipse-xtext-xbase-lib")
+ (version "2.25.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/eclipse/xtext-lib")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "13b9lf6lnsprkik665m1qcyyc8cs16k33xm7as4rjcfcpn4pln71"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "eclipse-xtext-xbase-lib.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; TODO
+ #:source-dir "org.eclipse.xtext.xbase.lib/src"
+ #:test-dir "org.eclipse.xtext.xbase.lib.tests/src"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-guava" ,java-guava)))
+ (home-page "https://www.eclipse.org/Xtext/")
+ (synopsis "Eclipse Xbase Runtime Library")
+ (description "This package contains runtime libraries for Xbase languages
+such as Xtend.")
+ (license license:epl2.0)))
+
(define-public java-javax-mail
(package
(name "java-javax-mail")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wHYACgkQjJF7f13F
G6LjlA/9Gjvyz5PIveWEiVO8trsnxADzGhUmdHPyVHekiAFANviiFrB5w/5f/VE1
Waa5tDeLAsRyubfHTXUpmp3lEQ+iIn4GRh4i8Mdck35ScJYx0YNoJLH0M621XbxE
CVS+NY8ZfzmHcp9hM/Ofp8pul1g08Q2wpTw8kRcb66mGedg6ePgZR0IDAqOhwCBY
yNlZsfxyQdN4DdYY7wq1cqptca9cQLd749deJCII4bzbXoTQnuBuIbPkTLb0EYUn
1ziCWUxcfZ4oG/H8aDQXCFAMFaQfvsMtGxTIBadVDh5ei3cLHjD4+aN5mUP2+cTw
ugIOwHRR3CZ30Xw5AtLUojCjhBlrdjLlAnXBNPGskq4GfNnfiyo4h8Uye5LHH5jH
HZjBsaOpfCrKyA0dnuW0kRr58Otm36GrJ4vQQSa/Qohekiw0mCYhn/QQ64rL4Qjy
gTI87Q/LPf7w4pqYCnP3+Omc/HYm6qYq0HvlopB78Z/QXdbcUsw1c8BhvnWD21nN
IuXjV4uAyxMBrl5kAOkniq8Ttn2dySuaNLjn6kkiF+aIWXiNzAumnUoqGsXVtN7y
xHcvNmn/K0N0ZZ5DkU+5QpZElz3pSGmI4OeylpJjBL3rlJ4Tp7+AQM3+PyKnyOkk
RLqBq//RTycbGqDK6JwzRB0XIXKNA26Pk07UPnfJaib3LLps6/Q=
=XG5v
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:26
[PATCH 3/6] gnu: Add java-eclipse-lsp4j packages.
(address . 47789@debbugs.gnu.org)
ac4dc52a97826de964853097feb19599ad630199.1618460450.git.mtg@gnu.org
All of these packages are components of java-eclipse-lsp4j, packaged
independently. This contains only what was needed for tla2tools, and so
there are parts of java-eclipse-lsp4j that are not packaged.

Note that this does not package the latest version (0.12.0 at the time
of writing)---it depends on the Xtend language, which is a huge
packaging effort. 0.10.0 is the version expected by tla2tools, for
which this dependency was introduced.

* gnu/packages/java.scm (java-eclipse-lsp4j-common): New variable.
(java-eclipse-lsp4j-jsonrpc): New variable.
(java-eclipse-lsp4j-jsonrpc-debug): New variable.
(java-eclipse-lsp4j-generator): New variable.
(java-eclipse-lsp4j-debug): New variable.
---
gnu/packages/java.scm | 104 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 104 insertions(+)

Toggle diff (120 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index b0e67b2f6e..e82e828df0 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -7547,6 +7547,110 @@ means for generating files and compiling new Java classes based on annotations
found in your source code.")
(license license:epl2.0)))
+(define java-eclipse-lsp4j-common
+ (package
+ (name "java-eclipse-lsp4j-common")
+ (version "0.10.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/eclipse/lsp4j")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "17srrac0pkpybwwc21rzdvn762zzl9m80rlqihc9b4l55hkqpk98"))))
+ (build-system ant-build-system)
+ (home-page "https://eclipse.org/lsp4j/")
+ (synopsis "LSP4J common package")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package is a common
+definition intended to be inherited by other packages.")
+ (license license:epl2.0)))
+
+(define-public java-eclipse-lsp4j-debug
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-debug")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-debug.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; tests fail obscurely
+ #:source-dir "org.eclipse.lsp4j.debug/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.debug/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-before 'build 'copy-xtend
+ (lambda _
+ (copy-recursively "org.eclipse.lsp4j.debug/src/main/xtend-gen"
+ "org.eclipse.lsp4j.debug/src/main/java")
+ #t)))))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-gson" ,java-gson-2.8.6)
+ ("java-eclipse-lsp4j-generaor" ,java-eclipse-lsp4j-generator)
+ ("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)
+ ("java-eclipse-lsp4j-jsonrpc-debug" ,java-eclipse-lsp4j-jsonrpc-debug)
+ ("java-eclipse-xtext-xbase-lib" ,java-eclipse-xtext-xbase-lib)))
+ (synopsis "Eclipse LSP4J Java bindings for the Debug Server Protocol")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+LSP4J Java bindings for the Debug Server Protocol.")))
+
+(define-public java-eclipse-lsp4j-generator
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-generator")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-generator.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; no tests
+ #:source-dir "org.eclipse.lsp4j.generator/src/main/java"))
+ (inputs
+ `(("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)))
+ (synopsis "Eclipse LSP4J Generator")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+LSP4J code generator for Language Server Protocol classes.")))
+
+(define-public java-eclipse-lsp4j-jsonrpc
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-jsonrpc")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-jsonrpc.jar"
+ #:jdk ,openjdk11
+ #:source-dir "org.eclipse.lsp4j.jsonrpc/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.jsonrpc/src/test"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-gson" ,java-gson-2.8.6)))
+ (synopsis "Java JSON-RPC implementation")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+JSON-RPC implementation.")))
+
+(define-public java-eclipse-lsp4j-jsonrpc-debug
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-jsonrpc-debug")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-jsonrpc-debug.jar"
+ #:jdk ,openjdk11
+ #:source-dir "org.eclipse.lsp4j.jsonrpc.debug/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.jsonrpc.debug/src/test"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)
+ ("java-gson" ,java-gson-2.8.6)))
+ (synopsis "Java JSON-RPC implementation (debug protocol)")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+JSON-RPC implementation's debug protocol.")))
+
(define-public java-eclipse-xtext-xbase-lib
(package
(name "java-eclipse-xtext-xbase-lib")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wIQACgkQjJF7f13F
G6J77RAAkUrTr0f+TCn710Sskp+tpSeyMwp1/IRPDBLTHLj3dAtxGYwnkGW06toL
D9Ty9M4IVDhRMl7PkDk7NPMRnVIj/Ez1cfqSlFRZCngNYWoPcSvbPHSflhkSp6v7
WOz1mmB1NjTuc4EApgCecG6UaVBGRMcL7Wfw1jMpzsAOlZ+YWi4162EzqJLQp/r6
4u81S+WEgPUcbnD0NP+aVrvCu5ZQGko3aCiWFIVeI5hzSbpeankOVSqVuk69KYvJ
9cQKYJZyGt1owQHdksHMyMGt0B8L7AU2i4MTL/wPhN6Xk/0afStQA5RGXaERA8PF
GN60U3kB7gLrHswGB8bp8QRpeUWxR8kgZMJiWGtABefHH4Q4Id4BA8OVX9BQmkI6
c8Jn+SNkS6dvI5vjDpi87Zbd/BPPZPum/u04x6ciuh0FqZ1opJx3foXFhscyrgCL
wxq6g60GlvWSN1QrkApUWM/aUAttAHbP9yUvAA4/McwnlqG9Mu9xSbwPHUwg58no
WAeNyuLPFt40Kq5MNrDUxI5HWg+/m3/3tJksmWBfWX8oceMs+VNCrgcnTq+UA31R
kx+IvWsyx4cOapyfN/H/pchgDP1arVo8c2Ae7gfLX94wAQ+1/AE8HvWL1ISY2z8O
UnnsoknPgK0LndHNlvyBVTNH5qJJMg9qWFw60wZFLAr8JvgN4wc=
=AyRh
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:26
[PATCH 4/6] gnu: Add java-jline-terminal.
(address . 47789@debbugs.gnu.org)
392710e13edd524ecac953dcecee73be459ea852.1618460450.git.mtg@gnu.org
This is part of JLine 3.

I was able to get this working properly under Guix by providing ncurses'
infocmp, as well as ensuring the *.caps files were present in the JAR,
but similar methods didn't work for the tests; if you have Java
knowledge, I'd appreciate the help getting those tests enabled.

* gnu/packages/java.scm (java-jline-terminal): New variable.
---
gnu/packages/java.scm | 57 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 57 insertions(+)

Toggle diff (80 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index e82e828df0..aef857661d 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -71,6 +71,7 @@
#:use-module (gnu packages maths)
#:use-module (gnu packages maven)
#:use-module (gnu packages maven-parent-pom)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages nss)
#:use-module (gnu packages onc-rpc)
#:use-module (gnu packages web)
@@ -12477,6 +12478,62 @@ features that bring it on par with the Z shell line editor.")
("java-junit" ,java-junit)
("java-hawtjni" ,java-hawtjni)))))
+(define-public java-jline-terminal
+ (package
+ (name "java-jline-terminal")
+ (version "3.14.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/jline/jline3")
+ (commit (string-append "jline-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0ilhk9ljp0pivl1rn0bb06syshc67p6imcjhrg6vr7kv15p3w4lr"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "jline-terminal.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; TODO: tests fail on *.caps resource lookups
+ #:source-dir "terminal/src/main/java"
+ #:test-dir "terminal/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-after 'unpack 'remove-build-file
+ (lambda _
+ ;; Conflicts with build directory generated by ant-build-system.
+ (delete-file "build")
+ #t))
+ (add-after 'unpack 'patch-paths
+ (lambda _
+ (substitute* "terminal/src/main/java/org/jline/utils/OSUtils.java"
+ (("= \"(s?tty|infocmp)\"" _ cmd)
+ (string-append "= \"" (which cmd) "\"")))
+ #t))
+ ;; Resources are not added to the JAR by ant-build-system.
+ (add-after 'build 'add-resources
+ (lambda* (#:key jar-name source-dir #:allow-other-keys)
+ (let ((build (string-append (getcwd) "/build")))
+ (with-directory-excursion
+ (string-append source-dir "/../resources")
+ (apply invoke "jar" "-uvf"
+ (string-append build "/jar/" jar-name)
+ (find-files "."))))
+ #t)))))
+ (inputs
+ `(("ncurses" ,ncurses))); infocmp
+ (home-page "https://github.com/jline/jline3")
+ (synopsis "Java JLine Terminal API and implementations")
+ (description "JLine is a Java library for handling console input. It is
+similar in functionality to BSD editline and GNU readline but with additional
+features that bring it in par with ZSH line editor. People familiar with the
+readline/editline capabilities for modern shells (such as bash and tcsh) will
+find most of the command editing features of JLine to be familiar.
+
+This package includes the @var{Terminal} API and implementations.")
+ (license license:bsd-3)))
+
(define-public java-xmlunit
(package
(name "java-xmlunit")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wJEACgkQjJF7f13F
G6KYPQ//dadG7AbdLkgzcYVY37ZHh1zjWVw4G30tkJNyKBCx9rUv+GAC/P7Ss516
wXr14MAX2Yn7Pa+F0bGI6FhwiEEsY2PkPbpJyi+Ug71g2YjjfGd0G+c7XBuqTngr
zMMxaAYhvngAyqc2W4CslY5nxj9WT0JigbvKuAgaPdhSTAgzwD+aYEop/rdWfRDi
ABj2fVZb1lx8/wkmUAhqRYFhzEHCIUVgGXPDmAUD4bz70DDi2YvpIGMBPjkQqi/W
rBLhSWKgZECyxBi8MJ6iOW+1Kff4sGLEU48+QzkLoFsa0LAhTpLtK9EwRaIvox2v
i5HoIJqMBLBckit74ED/cwLAeYgKz7LSmaHSCyeuiwpXm5ChIkLyLgykpH4oPg2m
YD+ivZOJKUNW8b6qWbqSMOIirP9XeyY/vJD25BpCIfh+etrMvAQHDNJ4Y7i/lhDJ
dcne/j158hVujd+e1ecrt+zat/yU7U2q+rxZcjeEoWnILb97DaL4GOoh/0+mHG4U
KK0R8Xup67OMppluEdA/klDiJ4HZ1RnTtRXfMht2NIOccC8hSy2KBSjFy2smo3vA
mYM9cwLNfosn1iAuOOXRmSVw9rMCxFG5EfqJej5w6glylNS+91EZ1/lJqK3Q3NoR
pdq/m8/rQPqf4P5BUiyqpedTGCydWDyfnIFg4eXgO9Ep5jMa490=
=fGE6
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:27
[PATCH 5/6] gnu: Add java-jline-reader.
(address . 47789@debbugs.gnu.org)
b10b57e88872629e09e5a3e30839380a450104f7.1618460451.git.mtg@gnu.org
This package is part of JLine 3.

* gnu/packages/java.scm (java-jline-reader): New variable.
---
gnu/packages/java.scm | 42 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 42 insertions(+)

Toggle diff (58 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index aef857661d..4d6befe511 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -12534,6 +12534,48 @@ find most of the command editing features of JLine to be familiar.
This package includes the @var{Terminal} API and implementations.")
(license license:bsd-3)))
+(define-public java-jline-reader
+ (package
+ (name "java-jline-reader")
+ (version "3.14.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/jline/jline3")
+ (commit (string-append "jline-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0ilhk9ljp0pivl1rn0bb06syshc67p6imcjhrg6vr7kv15p3w4lr"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "jline-reader.jar"
+ #:jdk ,openjdk11
+ #:source-dir "reader/src/main/java"
+ #:test-dir "reader/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-before 'build 'remove-build-file
+ (lambda _
+ ;; conflicts with build directory generated by ant-build-system
+ (delete-file "build")
+ #t)))))
+ (native-inputs
+ `(("java-junit" ,java-junit)
+ ("java-easymock" ,java-easymock)))
+ (inputs
+ `(("java-jline-terminal" ,java-jline-terminal)))
+ (home-page "https://github.com/jline/jline3")
+ (synopsis "Java JLine line reader")
+ (description "JLine is a Java library for handling console input. It is
+similar in functionality to BSD editline and GNU readline but with additional
+features that bring it in par with ZSH line editor. People familiar with the
+readline/editline capabilities for modern shells (such as bash and tcsh) will
+find most of the command editing features of JLine to be familiar.
+
+This package includes the line reader.")
+ (license license:bsd-3)))
+
(define-public java-xmlunit
(package
(name "java-xmlunit")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wKEACgkQjJF7f13F
G6LPgxAArhTGiQI9Ynr4mfDoDSiIBhd0fQKC6oq6g212sUnSCXXP7U4I+Jyz6+c3
mO7/ygvLEbPSqeg11syuyGwgqUueoJfp1RkP3Tab1JZdbpUKDCDNVMXkOmK2GwF+
Junu9bGI6JTJrHxenE4+GyTLiKhV2cdyFrho+VUptzFUJbcxoe/I4EJRJF5wxoJe
/mQS52YMpiRh+CO5mk7oq+9my2OjQ3jek9qnnMAYpjxH/OnycU28yFaok/Y4SDkU
AcBHMQUQTwEA1CNTXsoBWiuDXgQYyD9GrD3VqiDuTI+q75PC1Z5ALhtrX/eW/ICm
J4l9+KpiJe96SPm/KeN99sgxXH14lssA0QfOrk0PC3CVt6mg3va7Z4fDRNX8RUIw
N9K3TQX/Yp2nYoXZfIkWsBFNNg9SncdJJkc1RBNMfaVrmHXs6a4FBevRNrEDm4jL
IEs95xGTMG02hBO9DhYbj/4zrUXZOsZzKSDEr/pU9bDk6jZpGaTgTP2f7+lJeP6+
oKvE6BJN3mlBITJH9PmMk7R4avNXe9chVVabBbcch+TblCEX5fAtOef8Q1YCpyM0
vpc9m9PDkEMKxOkVn6jtCsmgBXjSTs4AHuT37hj4HLsjsnUTphDHLePfPMw+H6/v
lFmnavHpz3zxUHYVc7+nafp/7lLFStpPBAH/Ptf28OQCjBbfn+E=
=ok1u
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 15 Apr 2021 06:27
[PATCH 6/6] gnu: Add tla2tools.
(address . 47789@debbugs.gnu.org)
fc94440ebc83044f49813f58633ccaa6b1becc65.1618460451.git.mtg@gnu.org
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/packages/java.scm | 134 ++++++++++++++++++
.../patches/tla2tools-build-xml.patch | 109 ++++++++++++++
2 files changed, 243 insertions(+)
create mode 100644 gnu/packages/patches/tla2tools-build-xml.patch

Toggle diff (262 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 4d6befe511..087f411258 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -14040,3 +14040,137 @@ 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
+ "1503ljw32mbgw1mzkyk31sxdyggli9jf5sa31chfy5g5ccaphz9b"))
+ (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$"))
+ #t))))
+ (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))
+ #t))
+ (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$"))
+ #t))
+ (replace 'install
+ (lambda _
+ (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")))
+ (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
+ "#!" (which "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"))))
+ #t))))))
+ (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 -->
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wLEACgkQjJF7f13F
G6KB0g/8C5PjZ02yN2N8CANMJOFDRIiShnIGHsPuctVyY7yZ1iCGB4fLD6puG7UU
Okz+yCet46NEdJX8JewcomvxNx35p83Avo67koFxwcDHBzmStqW/fSxGyKjC8efX
gsjJ80sJuIIb9eBd3eSk7mFBzpWPKVByTF1+h6Ly43RLHeFDxvthIvnaKkX8AMWB
zcFSDXwnjo4gCUxHvL8iysnW/p1uG8wAIu/Fhx+VEWZGF/0SKLQdC84TlhaFqkw7
OrQ8VlEc/N4LC/I03vNnDIkifGRHothGV6oUKES0rLx6yppNey/59BWQ21OrQzrp
xAvepG8EpVj+2F0o8a6vZCZG3VNaLTkE9vzwHQB1fl/eDgH8/zBuiZ1DdlLK2jjx
80gk8HXahIjze5b0O3BkVTt09asRvzWuDHcB9Uqr9Tijb7xgGZ/FY1HNcvyMESIC
rgVnWJV1iVGinoe99W1o4b9vf8zASaxCMt2sZsDel4qHcbAvGdpQbMyiWeBJAIOb
DX805n2f+japhY1zNTIc+2MTYFbiXVIx3XTke6ht10e7mwYt1+czlY5jjxmkB55Z
XEZIZ4UyU15H/q/ehZZnU3y8l5sfZLGAKai+0axqmaU4YgTHe++ileY0MQXVidyh
PC6mmg2Fqh5cKffexiKmWiQzt0F1+y9WBvoE8ur81vDV1VKZyuM=
=jY2e
-----END PGP SIGNATURE-----

M
M
Maxime Devos wrote on 15 Apr 2021 10:06
Re: [bug#47789] [PATCH 1/6] gnu: Add java-gson-2.8.6.
eed2b30db3d7f6678e06ad217006d85155ea7bfa.camel@telenet.be
On Thu, 2021-04-15 at 00:25 -0400, Mike Gerwitz wrote:
Toggle quote (2 lines)
> + #t)))))

Phases do not need to return #t anymore. The warning has been removed
on the 'core-updates' branch; we might as well stop introducing these
silly #t now.

Greetings,
Maxime.
-----BEGIN PGP SIGNATURE-----

iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHfz6xccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7o3TAQCt2zyKDDuT2oH5gfOSaj+pQY/j
el6Rqu0RuOr/wY3W4QEAqaV6coHro2UMIbV/3VzGQLMBWaGDYvj93tbPb/TOZgE=
=hjJw
-----END PGP SIGNATURE-----


M
M
Maxime Devos wrote on 15 Apr 2021 10:13
Re: [bug#47789] [PATCH 4/6] gnu: Add java-jline-terminal.
5bcade8103a4995b6ba2fe64572c230bcbf52f82.camel@telenet.be
On Thu, 2021-04-15 at 00:26 -0400, Mike Gerwitz wrote:
Toggle quote (6 lines)
> + (add-after 'unpack 'patch-paths
> + (lambda _
> + (substitute* "terminal/src/main/java/org/jline/utils/OSUtils.java"
> + (("= \"(s?tty|infocmp)\"" _ cmd)
> + (string-append "= \"" (which cmd) "\"")))

(which cmd) is most likely incorrect when cross-compiling,
as when cross-compiling, only the inputs in "native-inputs" contribute
towards PATH, and "inputs" does not contribute towards PATH (IIUC).

You will need something like
(lambda* (#:key inputs #:allow-other-keys)
...
... (string-append "= \"" (assoc-ref "ncurses" inputs) "/bin/ncurses")
... (string-append "= \"" (assoc-ref "ncurses" inputs) "/bin/stty")
... (string-append "= \"" (assoc-ref "ncurses" inputs) "/bin/tty")
...)

(TODO to self: define a variant which/target which looks at the build inputs
instead of native-inputs when cross-compiling.)

Greetings,
Maxime.
-----BEGIN PGP SIGNATURE-----

iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHf1jxccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7ioVAQC04n7drXWkSlo87YmP+kNEJN4h
rcitHqcUSneyNCL/awD/UGAKzKAQyHpNLRhWZSVoN6ZUFOG6fpcZ34k4tM29wQ4=
=dMZQ
-----END PGP SIGNATURE-----


M
M
Maxime Devos wrote on 15 Apr 2021 10:17
Re: [bug#47789] [PATCH 6/6] gnu: Add tla2tools.
352cdaa9d0506cec61f4b086e1fae290938558e0.camel@telenet.be
On Thu, 2021-04-15 at 00:27 -0400, Mike Gerwitz wrote:
Toggle quote (1 lines)
> + "#!" (which "sh") "\n"
Most likely incorrect when cross-compiling, as noted in a previous
patch.

+ "java -cp " java-cp " " class " \"$@\""))))

Shouldn't this be "OPENJDK-11-FILENAME/bin/java ..."?

Greetings,
Maxime.
-----BEGIN PGP SIGNATURE-----

iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHf2hRccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7jj7AQDRtOiSGeWzGCK1bA3NW9Pe549+
Tus5XKGeuv4/51QwyAD/d0/wqKQK2UErxvqLIo1bz5CcPveFoDTx1YNQ0JOBEw8=
=rJiu
-----END PGP SIGNATURE-----


J
J
Julien Lepiller wrote on 15 Apr 2021 12:46
Re: [bug#47789] [PATCH 1/6] gnu: Add java-gson-2.8.6.
3EDAFE63-04AF-4D94-911E-B38BDFE0204A@lepiller.eu
Le 15 avril 2021 00:25:10 GMT-04:00, Mike Gerwitz <mtg@gnu.org> a écrit :
Toggle quote (83 lines)
>This introduces a new package rather than upgrading the exist java-gson
>package because it is built using OpenJDK11; I didn't want to have to
>propagate that JDK dependency to the other packages that use it.
>
>OpenJDK 11 was chosen becuase this dependency was introduced for
>tla2tools.
>
>* gnu/packages/java.scm (java-gson-2.8.6): New variable.
>---
> gnu/packages/java.scm | 43 +++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 43 insertions(+)
>
>diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
>index 207f136513..fe75404e9c 100644
>--- a/gnu/packages/java.scm
>+++ b/gnu/packages/java.scm
>@@ -15,6 +15,7 @@
> ;;; Copyright © 2020 Raghav Gururajan <raghavgururajan@disroot.org>
> ;;; Copyright © 2020 Maxim Cournoyer <maxim.cournoyer@gmail.com>
> ;;; Copyright © 2021 Vincent Legoll <vincent.legoll@gmail.com>
>+;;; Copyright © 2021 Mike Gerwitz <mtg@gnu.org>
> ;;;
> ;;; This file is part of GNU Guix.
> ;;;
>@@ -11724,6 +11725,48 @@ string to an equivalent Java object. Gson can
>work with arbitrary Java objects
> including pre-existing objects that you do not have source-code of.")
> (license license:asl2.0)))
>
>+;; This requires a different Java version than 2.8.2 above
>+(define-public java-gson-2.8.6
>+ (package
>+ (name "java-gson")
>+ (version "2.8.6")
>+ (source (origin
>+ (method git-fetch)
>+ (uri (git-reference
>+ (url "https://github.com/google/gson")
>+ (commit (string-append "gson-parent-" version))))
>+ (file-name (git-file-name name version))
>+ (sha256
>+ (base32
>+
>"0kk5p3vichdb0ph1lzknrcpbklgnmq455mngmjpxvvj29p3rgpk3"))))
>+ (build-system ant-build-system)
>+ (arguments
>+ `(#:jar-name "gson.jar"
>+ #:jdk ,openjdk11
>+ #:source-dir "gson/src/main/java"
>+ #:test-dir "gson/src/test"
>+ #:phases
>+ (modify-phases %standard-phases
>+ ;; avoid Maven dependency
>+ (add-before 'build 'fill-template
>+ (lambda _
>+ (with-directory-excursion "gson/src/main"
>+ (copy-file
>"java-templates/com/google/gson/internal/GsonBuildConfig.java"
>+
>"java/com/google/gson/internal/GsonBuildConfig.java")
>+ (substitute*
>"java/com/google/gson/internal/GsonBuildConfig.java"
>+ (("\\$\\{project.version\\}") ,version)))
>+ #t)))))
>+ (native-inputs
>+ `(("java-junit" ,java-junit)
>+ ("java-hamcrest-core" ,java-hamcrest-core)))
>+ (home-page "https://github.com/google/gson")
>+ (synopsis "Java serialization/deserialization library from/to
>JSON")
>+ (description "Gson is a Java library that can be used to convert
>Java
>+Objects into their JSON representation. It can also be used to
>convert a JSON
>+string to an equivalent Java object. Gson can work with arbitrary
>Java objects
>+including pre-existing objects that you do not have source-code of.")
>+ (license license:asl2.0)))
>+
> (define-public java-hawtjni
> (package
> (name "java-hawtjni")

Hi!

I think it would be easier to inherit from the existing package, right? Why do you need this package at all? I know that mixing JDKs can result in errors if you use a dependency that was built with a more recent JDK that what you use for a package, but the other way around should be fine, no?

What error do you get if you use the existing package?
M
M
Mike Gerwitz wrote on 16 Apr 2021 02:27
(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 47789@debbugs.gnu.org)
87lf9jm5tx.fsf@gnu.org
On Thu, Apr 15, 2021 at 06:46:21 -0400, Julien Lepiller wrote:
Toggle quote (3 lines)
> I think it would be easier to inherit from the existing package,
> right?

Thanks; a missed refactoring. I'll send an updated patch.

Toggle quote (4 lines)
> do you need this package at all? I know that mixing JDKs can result in
> errors if you use a dependency that was built with a more recent JDK that
> what you use for a package, but the other way around should be fine, no?

I suspect it'd be fine, but tla2tools uses what I assume is a new method
that wasn't in the previous API.

Toggle quote (2 lines)
> What error do you get if you use the existing package?

Toggle snippet (5 lines)
[javac] /tmp/guix-build-tla2tools-1.8.0.drv-0/tla2tools-1.8.0-checkout/tlatools/org.lamport.tlatools/src/tlc2/module/Json.java:116: error: cannot find symbol
[javac] JsonElement node = JsonParser.parseString(line);
[javac] ^

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB42g0ACgkQjJF7f13F
G6LK0xAAil8c2CwIlUbY/VNqJrUXRwxb7DUrv6AGEyxM9LTJ1r+WbVmaN/CK5yt0
XhtWdm76vrBz0l0aLJiyko1ggo9KUy9S5I5ru1tMfWSx7uz6VGCjXncR34rBL4zh
F4lrRfLbWV6W3ikvFokpiKmFUV1fYWJn9d7yEEXzb1lBCIbRHZSa3CHGSm86su+D
hgivmYM9bepd6Gbcz9F679YK8ZrNhEkAYXSpDEdRgTbh3YeZHw1/mEY463aYh4Js
Qv0l0TmLeQe3phh0om50yfKdM+KFTZ+V0NGHX8VcJdDBcKG37diiD5tJF20H2DVY
1NZSVee0npsOkA5owsATuThvSXVZut9vDwdXiRaOqcACptNWIsYd8TA28GqiiJsV
iP6UzBddUgwZPzF1POY78eTUVhiKMAeyrQQHdtDv1FQbMK4mXxYe2UaFKjQl2wIH
HfXVZ4h4RBd9AkrHenvjtUX2hBsRKUTGIS6madgiH2dg5yyBXdnbcLPMpCFXtZIJ
2wZz787V99wZJfBDVElGlWibt4m3lF5WrQBjFlIEDF4SPCJNiuTBLn9ZVcGeq12H
fD7RGLJwJR8WxzOiH9LXsTjGaxC+BMif4Uzm8pTDLUXkXVPFT6gH9n7nEemRq2lh
qfchCz+Wt3uRrdhobuCOW1/MSGY12MVxjTBWrLaKAN4IkyJEO1g=
=WlrE
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 02:55
Re: [bug#47789] [PATCH 4/6] gnu: Add java-jline-terminal.
(name . Maxime Devos)(address . maximedevos@telenet.be)(address . 47789@debbugs.gnu.org)
877dl3kpyd.fsf@gnu.org
On Thu, Apr 15, 2021 at 10:13:03 +0200, Maxime Devos wrote:
Toggle quote (16 lines)
> On Thu, 2021-04-15 at 00:26 -0400, Mike Gerwitz wrote:
>> + (add-after 'unpack 'patch-paths
>> + (lambda _
>> + (substitute* "terminal/src/main/java/org/jline/utils/OSUtils.java"
>> + (("= \"(s?tty|infocmp)\"" _ cmd)
>> + (string-append "= \"" (which cmd) "\"")))
>
> (which cmd) is most likely incorrect when cross-compiling,
> as when cross-compiling, only the inputs in "native-inputs" contribute
> towards PATH, and "inputs" does not contribute towards PATH (IIUC).
>
> You will need something like
> (lambda* (#:key inputs #:allow-other-keys)
> ...
> ... (string-append "= \"" (assoc-ref "ncurses" inputs) "/bin/ncurses")

Thanks. There are some other Java packages that do this as well. I'll
include these changes in the new series.

Toggle quote (3 lines)
> (TODO to self: define a variant which/target which looks at the build inputs
> instead of native-inputs when cross-compiling.)

+1

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB44J4ACgkQjJF7f13F
G6LC0RAAseO3EtswMnl207vCC50IoD5OeM2gcP2LwPIJltMCU0fx1+Q4RsJikMBM
JU1wOmO2V1WHUFC/BlFnB6POInVs4h5a4RDdZ2Gz9ZRWQj3bYAcZ2qwnzI8Xki7V
0Re8Qxr7CxVM6nQz63MFdNKFh5SAtDDjbQw20gAWKFPisuDvQHIFIanza2pIeO83
rFpMTnMuF66D15f9wJSx+dSgTEX8nnHqvFVqm2CiegXtAQKhyF63yXymLRNF4UIH
nxtkul0tL+/97wqgVG2U/taoQpXKr6jLRZQKHjpBvmGbrPezZdsNjq4s0hxiTNXm
SSFXh02/J037RUbFgH73XmF/34X7Mkn81Hhs6zSaSuPnAXuPfNTwZjrXrdy4sSJM
Tg4WNlgQLP34Av8z0udf/blf8FlKv9P+QaOp+T+NAKVo71I21AE1eP5dJW2NktF3
4HV68nB6GMl5kChAsOwtoVYvCCbIs8uodRQrCnzv5vqVZvMpR/ihXErzJvstrTbn
bOde2Dkj3hQKY2EMDoa3z5GEW1FFz1Y9VV0jjpf3C4+7dJQQ+a5NTPk8bXKKxztE
K90VceYj0w0Qb1ZdF/6boRulzMNUUHAQaO99C/1nEvlq2LrD+lNtantQoFnP+jV4
SJzpQvQYE7fm6vzmGmmS+jSRGht57T/qDtDibVhTnGYxVb2bZUA=
=SSbi
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 02:57
Re: [bug#47789] [PATCH 6/6] gnu: Add tla2tools.
(name . Maxime Devos)(address . maximedevos@telenet.be)(address . 47789@debbugs.gnu.org)
87y2djjbbx.fsf@gnu.org
On Thu, Apr 15, 2021 at 10:17:09 +0200, Maxime Devos wrote:
Toggle quote (9 lines)
> On Thu, 2021-04-15 at 00:27 -0400, Mike Gerwitz wrote:
>> + "#!" (which "sh") "\n"
> Most likely incorrect when cross-compiling, as noted in a previous
> patch.
>
> + "java -cp " java-cp " " class " \"$@\""))))
>
> Shouldn't this be "OPENJDK-11-FILENAME/bin/java ..."?

Indeed it should! Thanks. Fixed in the new series.

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB44OUACgkQjJF7f13F
G6LZIxAAgeVTD8hXqG/b4+GqNpujFTERW6cTcNTLaw+gvfs+5cWCds4hi8GfjEUS
xK97ZjNGgY4c3lEbvoMB/vRqoP+BCICPeJnOoVRObPg2MBb0aQvs5k3s8bLx1YMG
D6Ijh2aA+lGlOyfPeHloCplZMSD9+Sdwjytpz3EQ7gWuhWao+lyesut4MXObEOVS
0aXQE0XJkf0QNlihGXjDLszW6m8gfm3nj9QcnUDp211FWtOa0z9eW08behhLY2oN
cTaikP4VoPbUh13p9C7gS83qVRvDlHD+y+WUtEAB0WWtV4MTiypeLgT0qqHbFlYo
az00Sa//ZgmKvcnmGNYtgVU9jV2FNqAoFzg7fr4OawcO0a4bP3jkLVa/nfjZ65S5
LtGxRI0Wwkm99pUcrEICfI7cZDqO4TcozWqwq4ntj3wHa1Gpsi0+NDyW4EPwCpIs
KnFnjRe49dZFRrhoSb6jxZQMqPrxHjLCMN8Y/BY1X7Lxi8IOCADnxYyTV22u26lP
TM5uBKBljhRlxV9zPMXE+RvjsCn14k2dchc17bGiv0alnavCUGWBb/oVfb3TNfY7
tT1wgQDhLe/g3NkE7npwkzULfe4q4HpWpMY5p3ZmPWrp9VL0/r1dJhqQILKCoJqX
55UgINt7OMwdzhqv5mN+ekSslbwDR1pxRKUNmF2c8WvIAPkP25g=
=sDoi
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:12
(name . Maxime Devos)(address . maximedevos@telenet.be)(address . 47789@debbugs.gnu.org)
87im4njamo.fsf@gnu.org
On Thu, Apr 15, 2021 at 10:17:09 +0200, Maxime Devos wrote:
Toggle quote (5 lines)
> On Thu, 2021-04-15 at 00:27 -0400, Mike Gerwitz wrote:
>> + "#!" (which "sh") "\n"
> Most likely incorrect when cross-compiling, as noted in a previous
> patch.

I ended up using "/bin/sh" in the new series because the
'patch-source-shebangs phase that runs as part of the build system
automatically fixes it for me. Please lmk if that's not okay.

Using `(assoc-ref inputs "bash-minimal")' feels wrong to me since that
makes assumptions about the underlying dependencies, but I'll leave that
decision to you. (It didn't seem to work when I tried it, but I could
try again.)

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45fgACgkQjJF7f13F
G6J7kxAAl9K2EHNFiWtizm9kUZmxnoTZwoJMui7F0WT7Hu385PHbWN6ld68f6v4A
RMUFfQ5GA/MZ6i+w7Mok4MQWywuviaQUSQZ4ZKy7Zk/rBXHEDMSti3uUABEL6FUw
JI/BJNQ+prvZICUrCebpf2H6nEx0f7+wTCxe7b0tbdyRVYBmTkuwEIzv2AY+sJak
5vQt03cliPiIQoTVir8CMC4X6InMnI8Gt3h6PJaOF7azfpU8eqRZWdTMADzjgdn0
ZGo9ult5ABCPA0Ar0pjdwXNyxfBoihOUqw7iHX7GteUzeMTqiZqWjOrItVeV2KC5
9XOq/DtKzeHLb+xZmcRUloRA7KNryHqx0zCvch4BTJWhcn6u97QBGfxi+3dOks6o
EoHGL9dm6MIlgwOeWQl07V+HMbSkF6jiqyTnQbL4Dm0r4M1NLrGf9ZxD6MVEV4kW
PwqeLasmufyJZm1j+vMzN9zhVRewaCKIbeMAh++VOB+9UuhRCT5Pcaq/eYS/6kr+
pLMBzd1TeuqwhTXY1qdTgmLypUYgWeFTKAJkupxrNqgMO0ng8rYp8KHOZNkEa2TN
/EBBp/SyWAj1EUKNzwmYgl9tipgAsZjOFfWZ1ZAt3HaeBLHbZYgE1WTCMCmHsMwl
VuuhdJStZFtU6gwIY5XufEzcfolJKm7BhqI3P0hLCDqlfYuUNlM=
=TQNz
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:13
Re: [bug#47789] [PATCH 1/6] gnu: Add java-gson-2.8.6.
(name . Maxime Devos)(address . maximedevos@telenet.be)(address . 47789@debbugs.gnu.org)
87blafjal7.fsf@gnu.org
On Thu, Apr 15, 2021 at 10:06:03 +0200, Maxime Devos wrote:
Toggle quote (7 lines)
> On Thu, 2021-04-15 at 00:25 -0400, Mike Gerwitz wrote:
>> + #t)))))
>
> Phases do not need to return #t anymore. The warning has been removed
> on the 'core-updates' branch; we might as well stop introducing these
> silly #t now.

Corrected in each patch in the new series.

Thank you for your quick reviews!

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45KYACgkQjJF7f13F
G6LRrRAAxHvS8KbMqNo6xtVvKWdGjlHUpZgYqm8qx0LR1xeHDas96wHC6Adfy/kC
vDQbp1TX3erk9mamZO9VCh2FRoMRDEcCVSSvhq3nC0F6H5nc6DnC/bBM9RdRjl/Z
Npv737ANgZ5sLGokc0vFiXFR+NeK1qXtzuZwUpG+N0UQ5vKsThGub1UTz5/bVg0k
EZ6QbcoVj50vL3M5VvNO1SkDVRJVduDkMiHpYY2ovLo+IQsG7ycm6PDZ4VdBLip5
eHgeKSfrba04K9rfLpEIFYyA0aRdz+3BHie0uaRZdfXuoy9WJxb95W0rT9W227IC
w8KIBHcd+eD2VJMOh66+v6WTo8/5CDWXVHiLxk5DZ0550RTECna0bIc6wSjHfvIz
CzxjLEcLYdv3Z3ZbkP7sohIIr0OVja8qDopHx4ki87BgXiYSHyBBZ588KaDqNlEO
XlMlA0e+T7Q17fheJntGxWF0uWCdMx6QjjzNcXmFVU7hphVqEU6UHJd9eubrUn3a
ue3JyixjnI/7UnFODFX0bXDaEDNoYcrF69J/L92oPjD2fXlhku8c83Mn3zWxOFjq
5cFQMNwObFhcpfXzL5G8+bgDSvdlTN7uzHATzR7/eqMrwV+LWzZo/zhdLYRqA0Jr
W2TmrkFeiU6/MxgCWX/wpI+SbkBuI5htDo8P/aFxNzqzw0+EaO0=
=/pxV
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:23
[PATCH 1/6] gnu: Add java-gson-2.8.6.
(address . 47789@debbugs.gnu.org)
3f7bbd67919d869d70b267f8fd8d8edb90d59b65.1618536137.git.mtg@gnu.org
This introduces a new package rather than upgrading the exist java-gson
package because it is built using OpenJDK11; I didn't want to have to
propagate that JDK dependency to the other packages that use it.

OpenJDK 11 was chosen becuase this dependency was introduced for
tla2tools.

* gnu/packages/java.scm (java-gson-2.8.6): New variable.
---
gnu/packages/java.scm | 32 ++++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)

Toggle diff (55 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 207f136513..62f684a74c 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -15,6 +15,7 @@
;;; Copyright © 2020 Raghav Gururajan <raghavgururajan@disroot.org>
;;; Copyright © 2020 Maxim Cournoyer <maxim.cournoyer@gmail.com>
;;; Copyright © 2021 Vincent Legoll <vincent.legoll@gmail.com>
+;;; Copyright © 2021 Mike Gerwitz <mtg@gnu.org>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -11724,6 +11725,37 @@ string to an equivalent Java object. Gson can work with arbitrary Java objects
including pre-existing objects that you do not have source-code of.")
(license license:asl2.0)))
+;; This requires a different Java version than 2.8.2 above
+(define-public java-gson-2.8.6
+ (package
+ (inherit java-gson)
+ (name "java-gson")
+ (version "2.8.6")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/google/gson")
+ (commit (string-append "gson-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0kk5p3vichdb0ph1lzknrcpbklgnmq455mngmjpxvvj29p3rgpk3"))))
+ (arguments
+ `(#:jar-name "gson.jar"
+ #:jdk ,openjdk11
+ #:source-dir "gson/src/main/java"
+ #:test-dir "gson/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ ;; avoid Maven dependency
+ (add-before 'build 'fill-template
+ (lambda _
+ (with-directory-excursion "gson/src/main"
+ (copy-file "java-templates/com/google/gson/internal/GsonBuildConfig.java"
+ "java/com/google/gson/internal/GsonBuildConfig.java")
+ (substitute* "java/com/google/gson/internal/GsonBuildConfig.java"
+ (("\\$\\{project.version\\}") ,version))))))))))
+
(define-public java-hawtjni
(package
(name "java-hawtjni")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45yEACgkQjJF7f13F
G6LILA/8CGmJjPoz8oqxLwievO5/47umEbVNxJEQWl+O9HEYcodUrocXAU0ft8fL
VhiOC+2cksTog4NfpMDrn0GfN7+t1o2R144xyYsJHkjJyuAHDj9Y0QRII+Tt7bBk
MDC87YvgGEqD8zbF3B1xdZ+v5IBUJ7E+gCfizrntVBId/g4NgeEplXMjBHBQXNXY
/Vp1loYzEmaoFMwBo/ZHY0RxEm1/2Hcv3PeDOxjNVfP9s0ANiGx3Ck6atTAennwn
Ma6lJWzwLNPeCJXHXR04q4SXFIyBSPPm3Ii6nJ/oseTQ4O41qmlx/scQmTwDFRds
KDGRdvqKbQ42eGZxnJWjN9MKkEHEHQAWlptkIa/ga8D4Int6zL/sm1IR4hbbGEjT
uioQYEz99DwU9RH27XnJaYdB8qB9M9dxkPCBLfDvC6K0Oe/U14zNvSNwrl7s4dbB
6/bGAg1bvvZDABs5Aii4bUbK4OX6o1Icpv/NvYoo2V80eRS7UPpvmNX2mpiVNFea
3/h0fXbbS5uF+xsfmOJsPtl/D9zG6DG+ZGsLzsMhgmOmm9lwsKcwisSN3tjg4rVK
KKaSPA975tt5u38hg56xlFrqKgJxHcPYDawUv+p5BB2TIDFxZGj2xMQI3fb2Keau
IjtQEIcoUurIoZH31mbETiuqy7B+05b7XUMmO7aZfgKNfX1BgVA=
=xF35
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:23
[PATCH 2/6] gnu: Add java-eclipse-xtext-xbase-lib.
(address . 47789@debbugs.gnu.org)
90ad9b7f7ed8664cd041c6a8afa336539337dfd9.1618536137.git.mtg@gnu.org
This package is a component of xtext-lib. The rest of xtext-lib was not
added.

* gnu/packages/java.scm (java-eclipse-xtext-xbase-lib): New variable.
---
gnu/packages/java.scm | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)

Toggle diff (46 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 62f684a74c..4a80fef04f 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -7547,6 +7547,36 @@ means for generating files and compiling new Java classes based on annotations
found in your source code.")
(license license:epl2.0)))
+(define-public java-eclipse-xtext-xbase-lib
+ (package
+ (name "java-eclipse-xtext-xbase-lib")
+ (version "2.25.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/eclipse/xtext-lib")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "13b9lf6lnsprkik665m1qcyyc8cs16k33xm7as4rjcfcpn4pln71"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "eclipse-xtext-xbase-lib.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; TODO (maybe needs newer guava version?)
+ #:source-dir "org.eclipse.xtext.xbase.lib/src"
+ #:test-dir "org.eclipse.xtext.xbase.lib.tests/src"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-guava" ,java-guava)))
+ (home-page "https://www.eclipse.org/Xtext/")
+ (synopsis "Eclipse Xbase Runtime Library")
+ (description "This package contains runtime libraries for Xbase languages
+such as Xtend.")
+ (license license:epl2.0)))
+
(define-public java-javax-mail
(package
(name "java-javax-mail")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45ywACgkQjJF7f13F
G6JJww/8DxaC2UOwxsNgFfOySZrifJglckkU1VWDZYCIqCHWssPxizqUIpIEcgZR
Zsrnqg/WNgUIps6ey6ZDDUefR3W5vna3jg+Rk+OJhSilSb1U6Y57kaI7r6CaaR/K
HQWONkkcjcD1VPKejcTWd2yBNtPnM8eV+ZhW4rnYhvlvzoHKIFxHU9dh4TZGzQjQ
IoAz6M994/IA4ErkSEX2heTgGg+XStKc1kmLY0kjdbHl7dMqbTw3W9Nmyn3LAgtZ
1DEYbucouQibp6J2gy05VYDHrYRasw9M2VnQ4uXBfr+jij/WLb1IxDsMK99ql3r0
HCaiq/YEgamgvJvJFmpG8wk8qgHaJAQofgayVpOTiqzPbBNR12LvLD2GBh8LuKWT
88REX+ERacuG1iSlnBo5v/QvGQQpDt/EEM+XxEH5HY3P7oS31Cz5eO3EJ94Aatrj
SHwULFSq9bUYinP7nuXNCaFHeJKZ0Ax0/sVHuArfWYOpGwSwkE5k+rKHQAltl+p5
7pUOXdVG02/7GKlFjvFYtEijo0SArCqeQV2dpdkOYiKusgudNdxU6oCsZf/gk81n
t8EvssNoxCVlMppxlgVLLdYjNy69NzduTopznDJ3fy/FCDrocEJu7pmwDEtylKZ5
8cSAMRy/Ww+pLdTuRjPNHyKoSkBXMQVngTgMNj50zSxOlt2sMNg=
=R76u
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:24
[PATCH 3/6] gnu: Add java-eclipse-lsp4j packages.
(address . 47789@debbugs.gnu.org)
a52595a2ed12816b28996f513bb3e095ca548fea.1618536137.git.mtg@gnu.org
All of these packages are components of java-eclipse-lsp4j, packaged
independently. This contains only what was needed for tla2tools, and so
there are parts of java-eclipse-lsp4j that are not packaged.

Note that this does not package the latest version (0.12.0 at the time
of writing)---it depends on the Xtend language, which is a huge
packaging effort. 0.10.0 is the version expected by tla2tools, for
which this dependency was introduced.

* gnu/packages/java.scm (java-eclipse-lsp4j-common): New variable.
(java-eclipse-lsp4j-jsonrpc): New variable.
(java-eclipse-lsp4j-jsonrpc-debug): New variable.
(java-eclipse-lsp4j-generator): New variable.
(java-eclipse-lsp4j-debug): New variable.
---
gnu/packages/java.scm | 103 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 103 insertions(+)

Toggle diff (119 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 4a80fef04f..b4e4cafddb 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -7547,6 +7547,109 @@ means for generating files and compiling new Java classes based on annotations
found in your source code.")
(license license:epl2.0)))
+(define java-eclipse-lsp4j-common
+ (package
+ (name "java-eclipse-lsp4j-common")
+ (version "0.10.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/eclipse/lsp4j")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "17srrac0pkpybwwc21rzdvn762zzl9m80rlqihc9b4l55hkqpk98"))))
+ (build-system ant-build-system)
+ (home-page "https://eclipse.org/lsp4j/")
+ (synopsis "LSP4J common package")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package is a common
+definition intended to be inherited by other packages.")
+ (license license:epl2.0)))
+
+(define-public java-eclipse-lsp4j-debug
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-debug")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-debug.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; tests fail with reflection errors
+ #:source-dir "org.eclipse.lsp4j.debug/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.debug/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-before 'build 'copy-xtend
+ (lambda _
+ (copy-recursively "org.eclipse.lsp4j.debug/src/main/xtend-gen"
+ "org.eclipse.lsp4j.debug/src/main/java"))))))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-gson" ,java-gson-2.8.6)
+ ("java-eclipse-lsp4j-generaor" ,java-eclipse-lsp4j-generator)
+ ("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)
+ ("java-eclipse-lsp4j-jsonrpc-debug" ,java-eclipse-lsp4j-jsonrpc-debug)
+ ("java-eclipse-xtext-xbase-lib" ,java-eclipse-xtext-xbase-lib)))
+ (synopsis "Eclipse LSP4J Java bindings for the Debug Server Protocol")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+LSP4J Java bindings for the Debug Server Protocol.")))
+
+(define-public java-eclipse-lsp4j-generator
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-generator")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-generator.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; no tests
+ #:source-dir "org.eclipse.lsp4j.generator/src/main/java"))
+ (inputs
+ `(("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)))
+ (synopsis "Eclipse LSP4J Generator")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+LSP4J code generator for Language Server Protocol classes.")))
+
+(define-public java-eclipse-lsp4j-jsonrpc
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-jsonrpc")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-jsonrpc.jar"
+ #:jdk ,openjdk11
+ #:source-dir "org.eclipse.lsp4j.jsonrpc/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.jsonrpc/src/test"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-gson" ,java-gson-2.8.6)))
+ (synopsis "Java JSON-RPC implementation")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+JSON-RPC implementation.")))
+
+(define-public java-eclipse-lsp4j-jsonrpc-debug
+ (package
+ (inherit java-eclipse-lsp4j-common)
+ (name "java-eclipse-lsp4j-jsonrpc-debug")
+ (arguments
+ `(#:jar-name "eclipse-lsp4j-jsonrpc-debug.jar"
+ #:jdk ,openjdk11
+ #:source-dir "org.eclipse.lsp4j.jsonrpc.debug/src/main/java"
+ #:test-dir "org.eclipse.lsp4j.jsonrpc.debug/src/test"))
+ (native-inputs
+ `(("java-junit" ,java-junit)))
+ (inputs
+ `(("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)
+ ("java-gson" ,java-gson-2.8.6)))
+ (synopsis "Java JSON-RPC implementation (debug protocol)")
+ (description "Eclipse LSP4J provides Java bindings for the Language
+Server Protocol and the Debug Adapter Protocol. This package contains its
+JSON-RPC implementation's debug protocol.")))
+
(define-public java-eclipse-xtext-xbase-lib
(package
(name "java-eclipse-xtext-xbase-lib")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45zYACgkQjJF7f13F
G6JAEA//eV53GBp6S7bqPZ5kA0dmkpVq1Emelixf70eI0jx2PPFrst5AF2MEGrs3
VFt/s9f2wigofnxOgmP9F8zy5X2YX5YLHH+c8HtC6pjV7MSogbwMjLPFOwxFdV0i
WLAPFWbI0PmGOSrrk4yVctFW27cbIq+SLNG/JRvFWw/P+QLoNM2OwTbg6Zo9EQWa
EdaPvaBJpWHN+h0reC/jGBLxu13YlxQNmiVW9gCGBQUrLeNGHgCUlsb5pPCtpN+O
WzCZpREdB3NRER4RzsO7CRewKnA4CPPAPTypxz3HpMsBc5mTsdy+LqA4f0+Dwh9Y
mkCCyAUW2t1BBXme/ejdUOJw2XIoTdatHJafYSi6biTtSqKcilo45h4To1kfb3JJ
TQprt/2/NBlbkdkL/RrLKotiLz9vtyz6iNNxSTqZluLOpipKDdt/JaWfKatRMKU6
2XznXFjqR6WBmulkHMgvgnqn1C9fzJb9Yq9L5pbVHtKv8lZqZN4UkmCOZi8W6AnE
UZ+nGv4eDysMv0j14+HB6qWA9rOmfofMrTIKDCPSzWy7L3jUPQlhF4iQOZm0a/8M
l42yIFpEromEupxHYcWMOCEfuy7BT7QIsp93LYm+Neq4qXeXouMHoAC4FVPg/pC5
kTPiC6ZKLACAQbWyJJgCrcAXAaaaaDOHdhYKOgIxTHccWN4MwBg=
=Pyst
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:24
[PATCH 4/6] gnu: Add java-jline-terminal.
(address . 47789@debbugs.gnu.org)
180b7d0e03b1f00f1904471815cf987c75e061a6.1618536137.git.mtg@gnu.org
This is part of JLine 3.

I was able to get this working properly under Guix by providing ncurses'
infocmp, as well as ensuring the *.caps files were present in the JAR,
but similar methods didn't work for the tests; if you have Java
knowledge, I'd appreciate the help getting those tests enabled.

* gnu/packages/java.scm (java-jline-terminal): New variable.
---
gnu/packages/java.scm | 58 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)

Toggle diff (81 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index b4e4cafddb..9bf26b1dc7 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -71,6 +71,7 @@
#:use-module (gnu packages maths)
#:use-module (gnu packages maven)
#:use-module (gnu packages maven-parent-pom)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages nss)
#:use-module (gnu packages onc-rpc)
#:use-module (gnu packages web)
@@ -12465,6 +12466,63 @@ features that bring it on par with the Z shell line editor.")
("java-junit" ,java-junit)
("java-hawtjni" ,java-hawtjni)))))
+(define-public java-jline-terminal
+ (package
+ (name "java-jline-terminal")
+ (version "3.14.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/jline/jline3")
+ (commit (string-append "jline-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0ilhk9ljp0pivl1rn0bb06syshc67p6imcjhrg6vr7kv15p3w4lr"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "jline-terminal.jar"
+ #:jdk ,openjdk11
+ #:tests? #f; TODO: tests fail on *.caps resource lookups
+ #:source-dir "terminal/src/main/java"
+ #:test-dir "terminal/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-after 'unpack 'remove-build-file
+ (lambda _
+ ;; Conflicts with build directory generated by ant-build-system.
+ (delete-file "build")))
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "terminal/src/main/java/org/jline/utils/OSUtils.java"
+ (("= \"infocmp\"")
+ (string-append "= \"" (assoc-ref inputs "ncurses")
+ "/bin/infocmp\""))
+ (("= \"(s?tty)\"" _ cmd)
+ (string-append "= \"" (assoc-ref inputs "coreutils")
+ "/bin/" cmd "\"")))))
+ ;; Resources are not added to the JAR by ant-build-system.
+ (add-after 'build 'add-resources
+ (lambda* (#:key jar-name source-dir #:allow-other-keys)
+ (let ((build (string-append (getcwd) "/build")))
+ (with-directory-excursion
+ (string-append source-dir "/../resources")
+ (apply invoke "jar" "-uvf"
+ (string-append build "/jar/" jar-name)
+ (find-files ".")))))))))
+ (inputs
+ `(("ncurses" ,ncurses))); infocmp
+ (home-page "https://github.com/jline/jline3")
+ (synopsis "Java JLine Terminal API and implementations")
+ (description "JLine is a Java library for handling console input. It is
+similar in functionality to BSD editline and GNU readline but with additional
+features that bring it in par with ZSH line editor. People familiar with the
+readline/editline capabilities for modern shells (such as bash and tcsh) will
+find most of the command editing features of JLine to be familiar.
+
+This package includes the @var{Terminal} API and implementations.")
+ (license license:bsd-3)))
+
(define-public java-xmlunit
(package
(name "java-xmlunit")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB450IACgkQjJF7f13F
G6KpFw//TSP3+7OiRKDJPMCYW5ZRlVGQUWDqpRmspbL9M9/Q522P6Ad7Ev/xvQbF
eXf/NGPk6IKbqXKpDKAb/CFSLwoM7uoPfkuzwyQ9tZ85L4P1UOUPMVsupdE3wR1e
8bc/FL3VOdX67veHtGYMVSyNa+D/jw6/jt6hmoMagVqglsxJP1v/EJmGIFSw57mZ
3S38OaJxNH/aIsyCVGBzSU5SCgjY+vEiFYT5XbBnc48txRSdTi721Uk7wDsq0HH6
zc46Qh51bFq9BIf47cAYL7S5ZUs6tLAAO6gjMlZBJ/uTRdUQyW6atJ4J8I9gAkgV
JwMbYMI+oaBxjUD+MUOy20ytNM+dxIoBMd50eeoIA4pdwTug799gX31Vg/+Rorqf
Sa/qlavEGlxDcOBiodt+JpMk6ZzMnvCOK+QPj88CCBGnoUseKkyCXhZmdooTGj0d
QjiYAEinobp+/mq2C5pztqBqNGKHjCqGTEhrsR+p5NIzpNA2jP/ag4erQeG2m1LZ
s5khPKkBT8GvunuC1u+GyI08ftXjPHdan6IuAJRShDPlYrIp4pzFSTEcxYMFYxDD
Pva4DFlY6/M3c09ohRrkKL+K6r0LMhsqcjfRK8U/WsBP4uSOjgYTWUrfgD9GNYPJ
zybDVB/MGFJisuMpVDMzLePkNLKvGBtwDDCeWlq8q+afKPpP3V8=
=aWsF
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:24
[PATCH 5/6] gnu: Add java-jline-reader.
(address . 47789@debbugs.gnu.org)
ec42242cb183cb1a446d9eed3d683af5dd8bfbd9.1618536137.git.mtg@gnu.org
This package is part of JLine 3.

* gnu/packages/java.scm (java-jline-reader): New variable.
---
gnu/packages/java.scm | 41 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)

Toggle diff (57 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 9bf26b1dc7..a474c40ebb 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -12523,6 +12523,47 @@ find most of the command editing features of JLine to be familiar.
This package includes the @var{Terminal} API and implementations.")
(license license:bsd-3)))
+(define-public java-jline-reader
+ (package
+ (name "java-jline-reader")
+ (version "3.14.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/jline/jline3")
+ (commit (string-append "jline-parent-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0ilhk9ljp0pivl1rn0bb06syshc67p6imcjhrg6vr7kv15p3w4lr"))))
+ (build-system ant-build-system)
+ (arguments
+ `(#:jar-name "jline-reader.jar"
+ #:jdk ,openjdk11
+ #:source-dir "reader/src/main/java"
+ #:test-dir "reader/src/test"
+ #:phases
+ (modify-phases %standard-phases
+ (add-before 'build 'remove-build-file
+ (lambda _
+ ;; conflicts with build directory generated by ant-build-system
+ (delete-file "build"))))))
+ (native-inputs
+ `(("java-junit" ,java-junit)
+ ("java-easymock" ,java-easymock)))
+ (inputs
+ `(("java-jline-terminal" ,java-jline-terminal)))
+ (home-page "https://github.com/jline/jline3")
+ (synopsis "Java JLine line reader")
+ (description "JLine is a Java library for handling console input. It is
+similar in functionality to BSD editline and GNU readline but with additional
+features that bring it in par with ZSH line editor. People familiar with the
+readline/editline capabilities for modern shells (such as bash and tcsh) will
+find most of the command editing features of JLine to be familiar.
+
+This package includes the line reader.")
+ (license license:bsd-3)))
+
(define-public java-xmlunit
(package
(name "java-xmlunit")
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB4508ACgkQjJF7f13F
G6KvfRAAu+GYZbT0gctMXpY7NYjTlrGWLDHq7KZAxMmUCOi775KqMn3wiXiOo1Yq
aakbg4ffNK7Kt3vddNB9pl/8ZvMg2fVg3M9ixArJMfYelMgMNDdxLCkKcVi8otoZ
wAJQb7RXKDsjO4SiAAb+q5E7snMb0JdUmGF5IYiH5ZeVNmPG/Ic2eei5vF/tErta
q2fy2zak/oPQJtLXwfNIbpewTBNdrKqinj73G44D5FpSA4tgXZ4ZYAw38Jw05OXL
gbeGG4ufi18gh2YJr2K3yepAQmUsVVbyso1XEkVNkyVDG8XdB7N85Eakqtqu3Vbw
OmlDHQ90u3NyihKPZHDYUsF/kW+8p+0ZQSCRO20mC6+7my4FYumIDsFMYpw7mgXg
109ayDMEtkFagTDG6dPdPPeBHFShKGR9lCt8U5k85EL2nPvFe1O9VVKx/MhmoeFx
nNsumo2ML4lliyfWccZ8R0D5szUxwYkCVEozD2IZpy5I1W52CV6k5pvxVVU5tWXZ
+G3Egzs/Popa1OJkTiIpo/N+9H9gaXz6lQ7WXV+10dTPjlC0WHXoxHVzUJI/6MUL
rEeuXM4HXQr3poiKr3Pn4yYxkPjM+UHPGlFsI0YK6EBfY/U2AHjiXts46ZVgn5MJ
8yg3uhYYdZ3cuvyHGMRgyitsQYkQOOm7FIPcscBjMGSycYnQzJU=
=eAie
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:24
[PATCH 6/6] gnu: Add tla2tools.
(address . 47789@debbugs.gnu.org)
ebb4608d38a42da2076671603682f3e35ab53ebf.1618536137.git.mtg@gnu.org
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/packages/java.scm | 132 ++++++++++++++++++
.../patches/tla2tools-build-xml.patch | 109 +++++++++++++++
2 files changed, 241 insertions(+)
create mode 100644 gnu/packages/patches/tla2tools-build-xml.patch

Toggle diff (260 lines)
diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index a474c40ebb..12e3577ca4 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -14028,3 +14028,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
+ "1503ljw32mbgw1mzkyk31sxdyggli9jf5sa31chfy5g5ccaphz9b"))
+ (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 -->
--
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB451sACgkQjJF7f13F
G6ImbQ//UC9krmS4GYY1Bqd6yc0HOIMrUX1eL0SvZlPrA8kcbE/6XC2loAG7mrA+
guFGD+KcR8Qzjnm4m6NYpREkb1AvKT3v37TzuPjKxAOvNYls5rYyA9CvxdguW9O+
io2VkeeuJ97j4Sjtxiaxf0dpmDdAwtzKwUWMPUPatwbTYekA7ZZ1HW75FNpuHpQz
haoXmewD3YfBcQKwTceuGd2guvjl52SjCTfaOXBjtqotvGHgbte/63peVPv4f3G8
4jia39MHG7QDwrbA+nGjVkmmMhUYBzbrE+SrF8WIuovlg6MHLPpiErYjDcocalNS
XCPcCum0BWxCeWLlk77EmAdjJLVXceDiPVAApfaQI68zY5jGLOqm8lVjLaLMGKfx
lqKAYPvHAK4xeu+IDYwZFcrh/t68PljPuK3qt0YXg0n8T8U0MM1m+pModEKCcX+/
rtv80wVOpGtaCZ4/i+NUy6C4N7nne0LXJ/6vgk78zTB61EsGviFMY95t5qM3YkVz
e0dpKnQ8/K9xL+4v0aGbWwausuks35VGFj21FOqpdprZU2FaAoNbn2Vc6Wlg0nPF
D8vksv3dpZDxX8hnEq8ye19doA8YqFUNy7OpBAKNw7xiLTXVAZTRYfCxPoKkNqi/
cHjg8E6U8BC4iws5xvrhKcs5gVwA5p8V76kR/VFbKtb1/seGVk4=
=1cqh
-----END PGP SIGNATURE-----

M
M
Mike Gerwitz wrote on 16 Apr 2021 03:29
Re: [bug#47789] [PATCH 0/6] Add TLA+ Tools (tla2tools)
(address . 47789@debbugs.gnu.org)
87r1jbf249.fsf@gnu.org
Sorry, I sent the new series in reply to the original cover. :(

--
Mike Gerwitz
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB46JMACgkQjJF7f13F
G6LEqxAAnt6ANYAatsKqb7oTHa/gv9rtqYO/cD4FNybCmS9+dk3cBeDJvOeaRfKk
v3W26QPFejiFf8jfkL/yjaOmtYvjNSqmMAu6Jtxtkv18V/2nMVcMtSQaKUsMu2U7
cGMJG46Zq85TTiVA8mv8D1jQ+kcmlIVUOdK2Ch4YqS9DNrt9+TloEeIm/ZhPbXMN
aqorfEliob7SUzFV2kzl0RtGVZ3+Y8hI5zUgtDVEpAPc9WNdrkPGM1e1pjvYkP5D
t+pNeGQiTA0vF01LnUqAIZGdLjB2jJm/FfXg21F5p8pFTG8WMTjfw27mH5outklH
pm/GvNz1k0Si3xbnH/IlEDfdJGmuSzX81RPOy1FUiCahTDRMw1m6pAMIL7lMU8LQ
QJKE95t7YpiyXvn4JhNgO9GosYjTW9R3y2Ys4ux57wIS3HCorNI8ouewy08yf1iN
HL+yLdo9lG81B+aanmZSneos3Ov2BROC+AmBLj/dnksgIvAYPUITobU0nUCCUXz2
D6VFAQGAjbQx5JuR6kFJoXOBO+pn9cuK4NrZ2yPDwRt7rljIFd+eV0YEyuVYKyUH
tOZoTAyarPLHYLy5diM+Of/kocu31c/OWBiTZAGvv/077zIqHrA1zNDWhrc7FGnC
21FVb8QIdevHRou9JUqCmY/6PfOeoWBPCz/MvKur4IV4tUt0HDM=
=JAyl
-----END PGP SIGNATURE-----

L
L
Ludovic Courtès wrote on 5 May 2021 17:02
Re: bug#47789: [PATCH 0/6] Add TLA+ Tools (tla2tools)
(name . Mike Gerwitz)(address . mtg@gnu.org)(address . 47789-done@debbugs.gnu.org)
87y2cti5q1.fsf_-_@gnu.org
Hi Mike,

I pushed the whole patch series as
f30e8f29096e3ae2a4de689690daf5fa27a8c91b! \o/

For the tla2tools patch, I added the patch to gnu/local.mk. I also had
to change the hash of the checkout, because I wouldn’t get the same one.
There are two possibilities: either upstream changed the tag upstream,
or you were looking at a same-named store item actually coming from a
different commit. Please take a look and let us know if anything’s
amiss.

Thanks for this heroic effort, and apologies for the delay!

Ludo’.
Closed
?