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

DoneSubmitted by Mike Gerwitz.
Details
4 participants
  • Julien Lepiller
  • Ludovic Courtès
  • Maxime Devos
  • Mike Gerwitz
Owner
unassigned
Severity
normal
M
M
Mike Gerwitz wrote on 15 Apr 06:22 +0200
(address . guix-patches@gnu.org)
cover.1618460450.git.mtg@gnu.org
This introduces tla2tools.jar, which contains the TLA+ model checkerand simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeXtypesetting system; PlusCal translator; and more. I have added fivewrapper scripts for convenience, rather than invoking `java' manually.The wrapper scripts are not comprehensive; users who are familiar withtla2tools.jar, or have read the book Specifying Systems, may stillinvoke the commands in the traditional way.
This was significnatly more involved than I had anticipated, and I wasforced to make some compromises on how I handled dependencies. Mostnotably, rather than packaging the entirety of LSP4J and JLine 3, I packagedonly what tla2tools used, since going all the way would have been asignificant undertaking that I would not have been able to see through.
I have not packaged Java libraries for Guix before (and it's been yearssince I packaged anything else), so please be critical and let me know whatI can do better.
I hope to explore packaging TLAPS next. I don't anticipate packaging theToolbox for Guix, which is TLA+'s GUI; there are a huge number ofdependencies.
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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3v24ACgkQjJF7f13FG6JLtBAAjHMEfjqhCSaFk04meRrVvzE//XJOYfFyMpsqvASO354rKX/H3FT1iRuE585wcjv7DCsYruv+mTU9/eNYXgti8Q4e8l07PornvjXtMswi1R+XyqbbEmqHT8lJmhn4NsZ66zPHccd51jqraes5RX618sjWg7hj4BTc5bgB/DktLL5OBJnQFiVIk2/9O623zKiRCxjgWE2nUe4uwc52rlzKrR/8eSL4VlV5cE4VISrR1cd25toIr1pCgsbBCUkFP77oc+Tb2MRzrQ0nABfQe7yYoFwVrEwEfDWs2yQoJKxMYLJ+E37JMjdgEGwQ841wmOeJA1w5s5JP5twpMBBc0UX2F7PRM50F8+uXblMBW+/Ca+HCZLvRY3MnQNo6YQ3JCiUXiPtfeMufpmyLOcymFsnfGhodw50kdZ8BCNShESW9viEbQtk8H9auQZfFe9t4cvafdg9NCaFfQp2wF+b1fTGtiiO5IzFWJeBTFsYbymGKFsIX3qV4vtZH/2OCf8jE1Gd3lzZxybvykUszRrsDkO78diNgN1CnOVE6TtpVJ90ggGo50UJEIRK5dQJ9ulYJNNMx3M2KYzjnjKfdVGFRes7cDxzkF4CIxbyLiGORTj7AytNmrTBOdQlcbQ0jCattBrFFZn6tV2Jf3BNchUMCrBPz0CpB4sNo6BRuVh1sjzVtagQ==M6PH-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:25 +0200
[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-gsonpackage because it is built using OpenJDK11; I didn't want to have topropagate that JDK dependency to the other packages that use it.
OpenJDK 11 was chosen becuase this dependency was introduced fortla2tools.
* 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wCgACgkQjJF7f13FG6KmKA/+OS2SnWXIdcRLvPzy0C2fJxdCVRN76GJy5i3g9OU0ZrEBOtdGGBdnt9wLjSkuOb+9dnGz198B+g6bZAJ0/w+0SvaSUF7m1iD0scOc52KbWQ1MFxtZYUICJ5K9ow+Hfi9+ldMujgXNFaAzxKhyEbHiGVBlucDLGiXmvRMAUTICSkCGIC6AyEloM2Bh82M5K+/fMFR9oX1tkYn9H9rsvoq1TVxGaAvYzcss+aj/VttvmQPPfW9fd/ubyAZcTtOioybWTz65/5RouZSTsUcOyE5A/A0s78f408XJ6KlJvndmR8JUgnecbneHLteJBea0Sntn62MV3YxxCyBYR33Q00l+WyFhT97NADFJg4f/Ig7JGdxOz3/tflHh3XQInzf9L/4Ci6y608oXYS5C562RMgzLwg9SWZaj++KBWkV5sXNUkP0DTZyYzt1o6hMYDS0EG/Z8G6iCh9bKum71EE7D5BdVqcZJPjTd8cZjYG454DstiTF6LqGSamAcHfeoAjQyLVkSrJFNi+kFxmaMOJo5QsHnsMLFs09RCiC/x/UEq70WEbsrwP3wazsg5NtN72Jvyo6EjHzRbMpPJMkkqqtUFiuPM6HK9k2StHeqT68PFr0YMC6oy0VM9ZsD+GyhjkA6D7I4UTxiw9DiFUq5HaGLziXsaqeN9fH7PglCNjgf557tOJs==1Mmw-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:26 +0200
[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 notadded.
* 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wHYACgkQjJF7f13FG6LjlA/9Gjvyz5PIveWEiVO8trsnxADzGhUmdHPyVHekiAFANviiFrB5w/5f/VE1Waa5tDeLAsRyubfHTXUpmp3lEQ+iIn4GRh4i8Mdck35ScJYx0YNoJLH0M621XbxECVS+NY8ZfzmHcp9hM/Ofp8pul1g08Q2wpTw8kRcb66mGedg6ePgZR0IDAqOhwCBYyNlZsfxyQdN4DdYY7wq1cqptca9cQLd749deJCII4bzbXoTQnuBuIbPkTLb0EYUn1ziCWUxcfZ4oG/H8aDQXCFAMFaQfvsMtGxTIBadVDh5ei3cLHjD4+aN5mUP2+cTwugIOwHRR3CZ30Xw5AtLUojCjhBlrdjLlAnXBNPGskq4GfNnfiyo4h8Uye5LHH5jHHZjBsaOpfCrKyA0dnuW0kRr58Otm36GrJ4vQQSa/Qohekiw0mCYhn/QQ64rL4QjygTI87Q/LPf7w4pqYCnP3+Omc/HYm6qYq0HvlopB78Z/QXdbcUsw1c8BhvnWD21nNIuXjV4uAyxMBrl5kAOkniq8Ttn2dySuaNLjn6kkiF+aIWXiNzAumnUoqGsXVtN7yxHcvNmn/K0N0ZZ5DkU+5QpZElz3pSGmI4OeylpJjBL3rlJ4Tp7+AQM3+PyKnyOkkRLqBq//RTycbGqDK6JwzRB0XIXKNA26Pk07UPnfJaib3LLps6/Q==XG5v-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:26 +0200
[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, packagedindependently. This contains only what was needed for tla2tools, and sothere are parts of java-eclipse-lsp4j that are not packaged.
Note that this does not package the latest version (0.12.0 at the timeof writing)---it depends on the Xtend language, which is a hugepackaging effort. 0.10.0 is the version expected by tla2tools, forwhich 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wIQACgkQjJF7f13FG6J77RAAkUrTr0f+TCn710Sskp+tpSeyMwp1/IRPDBLTHLj3dAtxGYwnkGW06toLD9Ty9M4IVDhRMl7PkDk7NPMRnVIj/Ez1cfqSlFRZCngNYWoPcSvbPHSflhkSp6v7WOz1mmB1NjTuc4EApgCecG6UaVBGRMcL7Wfw1jMpzsAOlZ+YWi4162EzqJLQp/r64u81S+WEgPUcbnD0NP+aVrvCu5ZQGko3aCiWFIVeI5hzSbpeankOVSqVuk69KYvJ9cQKYJZyGt1owQHdksHMyMGt0B8L7AU2i4MTL/wPhN6Xk/0afStQA5RGXaERA8PFGN60U3kB7gLrHswGB8bp8QRpeUWxR8kgZMJiWGtABefHH4Q4Id4BA8OVX9BQmkI6c8Jn+SNkS6dvI5vjDpi87Zbd/BPPZPum/u04x6ciuh0FqZ1opJx3foXFhscyrgCLwxq6g60GlvWSN1QrkApUWM/aUAttAHbP9yUvAA4/McwnlqG9Mu9xSbwPHUwg58noWAeNyuLPFt40Kq5MNrDUxI5HWg+/m3/3tJksmWBfWX8oceMs+VNCrgcnTq+UA31Rkx+IvWsyx4cOapyfN/H/pchgDP1arVo8c2Ae7gfLX94wAQ+1/AE8HvWL1ISY2z8OUnnsoknPgK0LndHNlvyBVTNH5qJJMg9qWFw60wZFLAr8JvgN4wc==AyRh-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:26 +0200
[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 Javaknowledge, 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wJEACgkQjJF7f13FG6KYPQ//dadG7AbdLkgzcYVY37ZHh1zjWVw4G30tkJNyKBCx9rUv+GAC/P7Ss516wXr14MAX2Yn7Pa+F0bGI6FhwiEEsY2PkPbpJyi+Ug71g2YjjfGd0G+c7XBuqTngrzMMxaAYhvngAyqc2W4CslY5nxj9WT0JigbvKuAgaPdhSTAgzwD+aYEop/rdWfRDiABj2fVZb1lx8/wkmUAhqRYFhzEHCIUVgGXPDmAUD4bz70DDi2YvpIGMBPjkQqi/WrBLhSWKgZECyxBi8MJ6iOW+1Kff4sGLEU48+QzkLoFsa0LAhTpLtK9EwRaIvox2vi5HoIJqMBLBckit74ED/cwLAeYgKz7LSmaHSCyeuiwpXm5ChIkLyLgykpH4oPg2mYD+ivZOJKUNW8b6qWbqSMOIirP9XeyY/vJD25BpCIfh+etrMvAQHDNJ4Y7i/lhDJdcne/j158hVujd+e1ecrt+zat/yU7U2q+rxZcjeEoWnILb97DaL4GOoh/0+mHG4UKK0R8Xup67OMppluEdA/klDiJ4HZ1RnTtRXfMht2NIOccC8hSy2KBSjFy2smo3vAmYM9cwLNfosn1iAuOOXRmSVw9rMCxFG5EfqJej5w6glylNS+91EZ1/lJqK3Q3NoRpdq/m8/rQPqf4P5BUiyqpedTGCydWDyfnIFg4eXgO9Ep5jMa490==fGE6-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:27 +0200
[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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wKEACgkQjJF7f13FG6LPgxAArhTGiQI9Ynr4mfDoDSiIBhd0fQKC6oq6g212sUnSCXXP7U4I+Jyz6+c3mO7/ygvLEbPSqeg11syuyGwgqUueoJfp1RkP3Tab1JZdbpUKDCDNVMXkOmK2GwF+Junu9bGI6JTJrHxenE4+GyTLiKhV2cdyFrho+VUptzFUJbcxoe/I4EJRJF5wxoJe/mQS52YMpiRh+CO5mk7oq+9my2OjQ3jek9qnnMAYpjxH/OnycU28yFaok/Y4SDkUAcBHMQUQTwEA1CNTXsoBWiuDXgQYyD9GrD3VqiDuTI+q75PC1Z5ALhtrX/eW/ICmJ4l9+KpiJe96SPm/KeN99sgxXH14lssA0QfOrk0PC3CVt6mg3va7Z4fDRNX8RUIwN9K3TQX/Yp2nYoXZfIkWsBFNNg9SncdJJkc1RBNMfaVrmHXs6a4FBevRNrEDm4jLIEs95xGTMG02hBO9DhYbj/4zrUXZOsZzKSDEr/pU9bDk6jZpGaTgTP2f7+lJeP6+oKvE6BJN3mlBITJH9PmMk7R4avNXe9chVVabBbcch+TblCEX5fAtOef8Q1YCpyM0vpc9m9PDkEMKxOkVn6jtCsmgBXjSTs4AHuT37hj4HLsjsnUTphDHLePfPMw+H6/vlFmnavHpz3zxUHYVc7+nafp/7lLFStpPBAH/Ptf28OQCjBbfn+E==ok1u-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 15 Apr 06:27 +0200
[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 checkerand simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeXtypesetting system; PlusCal translator; and more. I have added fivewrapper scripts for convenience, rather than invoking `java' manually.The wrapper scripts are not comprehensive; users who are familiar withtla2tools.jar, or have read the book Specifying Systems, may stillinvoke the commands in the traditional way.
The minimum JDK version is 11. I chose to stick with that rather thanbumping 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 unnecessarydependencies.
Note that this is _not_ the TLA+ Toolbox, which is the GUI commonly usedwith 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.scmindex 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.patchnew file mode 100644index 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB3wLEACgkQjJF7f13FG6KB0g/8C5PjZ02yN2N8CANMJOFDRIiShnIGHsPuctVyY7yZ1iCGB4fLD6puG7UUOkz+yCet46NEdJX8JewcomvxNx35p83Avo67koFxwcDHBzmStqW/fSxGyKjC8efXgsjJ80sJuIIb9eBd3eSk7mFBzpWPKVByTF1+h6Ly43RLHeFDxvthIvnaKkX8AMWBzcFSDXwnjo4gCUxHvL8iysnW/p1uG8wAIu/Fhx+VEWZGF/0SKLQdC84TlhaFqkw7OrQ8VlEc/N4LC/I03vNnDIkifGRHothGV6oUKES0rLx6yppNey/59BWQ21OrQzrpxAvepG8EpVj+2F0o8a6vZCZG3VNaLTkE9vzwHQB1fl/eDgH8/zBuiZ1DdlLK2jjx80gk8HXahIjze5b0O3BkVTt09asRvzWuDHcB9Uqr9Tijb7xgGZ/FY1HNcvyMESICrgVnWJV1iVGinoe99W1o4b9vf8zASaxCMt2sZsDel4qHcbAvGdpQbMyiWeBJAIObDX805n2f+japhY1zNTIc+2MTYFbiXVIx3XTke6ht10e7mwYt1+czlY5jjxmkB55ZXEZIZ4UyU15H/q/ehZZnU3y8l5sfZLGAKai+0axqmaU4YgTHe++ileY0MQXVidyhPC6mmg2Fqh5cKffexiKmWiQzt0F1+y9WBvoE8ur81vDV1VKZyuM==jY2e-----END PGP SIGNATURE-----
M
M
Maxime Devos wrote on 15 Apr 10:06 +0200
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 removedon the 'core-updates' branch; we might as well stop introducing thesesilly #t now.
Greetings,Maxime.
-----BEGIN PGP SIGNATURE-----
iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHfz6xccbWF4aW1lZGV2b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7o3TAQCt2zyKDDuT2oH5gfOSaj+pQY/jel6Rqu0RuOr/wY3W4QEAqaV6coHro2UMIbV/3VzGQLMBWaGDYvj93tbPb/TOZgE==hjJw-----END PGP SIGNATURE-----

M
M
Maxime Devos wrote on 15 Apr 10:13 +0200
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" contributetowards 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 inputsinstead of native-inputs when cross-compiling.)
Greetings,Maxime.
-----BEGIN PGP SIGNATURE-----
iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHf1jxccbWF4aW1lZGV2b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7ioVAQC04n7drXWkSlo87YmP+kNEJN4hrcitHqcUSneyNCL/awD/UGAKzKAQyHpNLRhWZSVoN6ZUFOG6fpcZ34k4tM29wQ4==dMZQ-----END PGP SIGNATURE-----

M
M
Maxime Devos wrote on 15 Apr 10:17 +0200
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 previouspatch.
+ "java -cp " java-cp " " class " \"$@\""))))
Shouldn't this be "OPENJDK-11-FILENAME/bin/java ..."?
Greetings,Maxime.
-----BEGIN PGP SIGNATURE-----
iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYHf2hRccbWF4aW1lZGV2b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7jj7AQDRtOiSGeWzGCK1bA3NW9Pe549+Tus5XKGeuv4/51QwyAD/d0/wqKQK2UErxvqLIo1bz5CcPveFoDTx1YNQ0JOBEw8==rJiu-----END PGP SIGNATURE-----

J
J
Julien Lepiller wrote on 15 Apr 12:46 +0200
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 02:27 +0200
(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 methodthat 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-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB42g0ACgkQjJF7f13FG6LK0xAAil8c2CwIlUbY/VNqJrUXRwxb7DUrv6AGEyxM9LTJ1r+WbVmaN/CK5yt0XhtWdm76vrBz0l0aLJiyko1ggo9KUy9S5I5ru1tMfWSx7uz6VGCjXncR34rBL4zhF4lrRfLbWV6W3ikvFokpiKmFUV1fYWJn9d7yEEXzb1lBCIbRHZSa3CHGSm86su+DhgivmYM9bepd6Gbcz9F679YK8ZrNhEkAYXSpDEdRgTbh3YeZHw1/mEY463aYh4JsQv0l0TmLeQe3phh0om50yfKdM+KFTZ+V0NGHX8VcJdDBcKG37diiD5tJF20H2DVY1NZSVee0npsOkA5owsATuThvSXVZut9vDwdXiRaOqcACptNWIsYd8TA28GqiiJsViP6UzBddUgwZPzF1POY78eTUVhiKMAeyrQQHdtDv1FQbMK4mXxYe2UaFKjQl2wIHHfXVZ4h4RBd9AkrHenvjtUX2hBsRKUTGIS6madgiH2dg5yyBXdnbcLPMpCFXtZIJ2wZz787V99wZJfBDVElGlWibt4m3lF5WrQBjFlIEDF4SPCJNiuTBLn9ZVcGeq12HfD7RGLJwJR8WxzOiH9LXsTjGaxC+BMif4Uzm8pTDLUXkXVPFT6gH9n7nEemRq2lhqfchCz+Wt3uRrdhobuCOW1/MSGY12MVxjTBWrLaKAN4IkyJEO1g==WlrE-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 02:55 +0200
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'llinclude 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-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB44J4ACgkQjJF7f13FG6LC0RAAseO3EtswMnl207vCC50IoD5OeM2gcP2LwPIJltMCU0fx1+Q4RsJikMBMJU1wOmO2V1WHUFC/BlFnB6POInVs4h5a4RDdZ2Gz9ZRWQj3bYAcZ2qwnzI8Xki7V0Re8Qxr7CxVM6nQz63MFdNKFh5SAtDDjbQw20gAWKFPisuDvQHIFIanza2pIeO83rFpMTnMuF66D15f9wJSx+dSgTEX8nnHqvFVqm2CiegXtAQKhyF63yXymLRNF4UIHnxtkul0tL+/97wqgVG2U/taoQpXKr6jLRZQKHjpBvmGbrPezZdsNjq4s0hxiTNXmSSFXh02/J037RUbFgH73XmF/34X7Mkn81Hhs6zSaSuPnAXuPfNTwZjrXrdy4sSJMTg4WNlgQLP34Av8z0udf/blf8FlKv9P+QaOp+T+NAKVo71I21AE1eP5dJW2NktF34HV68nB6GMl5kChAsOwtoVYvCCbIs8uodRQrCnzv5vqVZvMpR/ihXErzJvstrTbnbOde2Dkj3hQKY2EMDoa3z5GEW1FFz1Y9VV0jjpf3C4+7dJQQ+a5NTPk8bXKKxztEK90VceYj0w0Qb1ZdF/6boRulzMNUUHAQaO99C/1nEvlq2LrD+lNtantQoFnP+jV4SJzpQvQYE7fm6vzmGmmS+jSRGht57T/qDtDibVhTnGYxVb2bZUA==SSbi-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 02:57 +0200
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-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB44OUACgkQjJF7f13FG6LZIxAAgeVTD8hXqG/b4+GqNpujFTERW6cTcNTLaw+gvfs+5cWCds4hi8GfjEUSxK97ZjNGgY4c3lEbvoMB/vRqoP+BCICPeJnOoVRObPg2MBb0aQvs5k3s8bLx1YMGD6Ijh2aA+lGlOyfPeHloCplZMSD9+Sdwjytpz3EQ7gWuhWao+lyesut4MXObEOVS0aXQE0XJkf0QNlihGXjDLszW6m8gfm3nj9QcnUDp211FWtOa0z9eW08behhLY2oNcTaikP4VoPbUh13p9C7gS83qVRvDlHD+y+WUtEAB0WWtV4MTiypeLgT0qqHbFlYoaz00Sa//ZgmKvcnmGNYtgVU9jV2FNqAoFzg7fr4OawcO0a4bP3jkLVa/nfjZ65S5LtGxRI0Wwkm99pUcrEICfI7cZDqO4TcozWqwq4ntj3wHa1Gpsi0+NDyW4EPwCpIsKnFnjRe49dZFRrhoSb6jxZQMqPrxHjLCMN8Y/BY1X7Lxi8IOCADnxYyTV22u26lPTM5uBKBljhRlxV9zPMXE+RvjsCn14k2dchc17bGiv0alnavCUGWBb/oVfb3TNfY7tT1wgQDhLe/g3NkE7npwkzULfe4q4HpWpMY5p3ZmPWrp9VL0/r1dJhqQILKCoJqX55UgINt7OMwdzhqv5mN+ekSslbwDR1pxRKUNmF2c8WvIAPkP25g==sDoi-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:12 +0200
(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 systemautomatically fixes it for me. Please lmk if that's not okay.
Using `(assoc-ref inputs "bash-minimal")' feels wrong to me since thatmakes assumptions about the underlying dependencies, but I'll leave thatdecision to you. (It didn't seem to work when I tried it, but I couldtry again.)
-- Mike Gerwitz
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45fgACgkQjJF7f13FG6J7kxAAl9K2EHNFiWtizm9kUZmxnoTZwoJMui7F0WT7Hu385PHbWN6ld68f6v4ARMUFfQ5GA/MZ6i+w7Mok4MQWywuviaQUSQZ4ZKy7Zk/rBXHEDMSti3uUABEL6FUwJI/BJNQ+prvZICUrCebpf2H6nEx0f7+wTCxe7b0tbdyRVYBmTkuwEIzv2AY+sJak5vQt03cliPiIQoTVir8CMC4X6InMnI8Gt3h6PJaOF7azfpU8eqRZWdTMADzjgdn0ZGo9ult5ABCPA0Ar0pjdwXNyxfBoihOUqw7iHX7GteUzeMTqiZqWjOrItVeV2KC59XOq/DtKzeHLb+xZmcRUloRA7KNryHqx0zCvch4BTJWhcn6u97QBGfxi+3dOks6oEoHGL9dm6MIlgwOeWQl07V+HMbSkF6jiqyTnQbL4Dm0r4M1NLrGf9ZxD6MVEV4kWPwqeLasmufyJZm1j+vMzN9zhVRewaCKIbeMAh++VOB+9UuhRCT5Pcaq/eYS/6kr+pLMBzd1TeuqwhTXY1qdTgmLypUYgWeFTKAJkupxrNqgMO0ng8rYp8KHOZNkEa2TN/EBBp/SyWAj1EUKNzwmYgl9tipgAsZjOFfWZ1ZAt3HaeBLHbZYgE1WTCMCmHsMwlVuuhdJStZFtU6gwIY5XufEzcfolJKm7BhqI3P0hLCDqlfYuUNlM==TQNz-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:13 +0200
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-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45KYACgkQjJF7f13FG6LRrRAAxHvS8KbMqNo6xtVvKWdGjlHUpZgYqm8qx0LR1xeHDas96wHC6Adfy/kCvDQbp1TX3erk9mamZO9VCh2FRoMRDEcCVSSvhq3nC0F6H5nc6DnC/bBM9RdRjl/ZNpv737ANgZ5sLGokc0vFiXFR+NeK1qXtzuZwUpG+N0UQ5vKsThGub1UTz5/bVg0kEZ6QbcoVj50vL3M5VvNO1SkDVRJVduDkMiHpYY2ovLo+IQsG7ycm6PDZ4VdBLip5eHgeKSfrba04K9rfLpEIFYyA0aRdz+3BHie0uaRZdfXuoy9WJxb95W0rT9W227ICw8KIBHcd+eD2VJMOh66+v6WTo8/5CDWXVHiLxk5DZ0550RTECna0bIc6wSjHfvIzCzxjLEcLYdv3Z3ZbkP7sohIIr0OVja8qDopHx4ki87BgXiYSHyBBZ588KaDqNlEOXlMlA0e+T7Q17fheJntGxWF0uWCdMx6QjjzNcXmFVU7hphVqEU6UHJd9eubrUn3aue3JyixjnI/7UnFODFX0bXDaEDNoYcrF69J/L92oPjD2fXlhku8c83Mn3zWxOFjq5cFQMNwObFhcpfXzL5G8+bgDSvdlTN7uzHATzR7/eqMrwV+LWzZo/zhdLYRqA0JrW2TmrkFeiU6/MxgCWX/wpI+SbkBuI5htDo8P/aFxNzqzw0+EaO0==/pxV-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:23 +0200
[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-gsonpackage because it is built using OpenJDK11; I didn't want to have topropagate that JDK dependency to the other packages that use it.
OpenJDK 11 was chosen becuase this dependency was introduced fortla2tools.
* 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45yEACgkQjJF7f13FG6LILA/8CGmJjPoz8oqxLwievO5/47umEbVNxJEQWl+O9HEYcodUrocXAU0ft8fLVhiOC+2cksTog4NfpMDrn0GfN7+t1o2R144xyYsJHkjJyuAHDj9Y0QRII+Tt7bBkMDC87YvgGEqD8zbF3B1xdZ+v5IBUJ7E+gCfizrntVBId/g4NgeEplXMjBHBQXNXY/Vp1loYzEmaoFMwBo/ZHY0RxEm1/2Hcv3PeDOxjNVfP9s0ANiGx3Ck6atTAennwnMa6lJWzwLNPeCJXHXR04q4SXFIyBSPPm3Ii6nJ/oseTQ4O41qmlx/scQmTwDFRdsKDGRdvqKbQ42eGZxnJWjN9MKkEHEHQAWlptkIa/ga8D4Int6zL/sm1IR4hbbGEjTuioQYEz99DwU9RH27XnJaYdB8qB9M9dxkPCBLfDvC6K0Oe/U14zNvSNwrl7s4dbB6/bGAg1bvvZDABs5Aii4bUbK4OX6o1Icpv/NvYoo2V80eRS7UPpvmNX2mpiVNFea3/h0fXbbS5uF+xsfmOJsPtl/D9zG6DG+ZGsLzsMhgmOmm9lwsKcwisSN3tjg4rVKKKaSPA975tt5u38hg56xlFrqKgJxHcPYDawUv+p5BB2TIDFxZGj2xMQI3fb2KeauIjtQEIcoUurIoZH31mbETiuqy7B+05b7XUMmO7aZfgKNfX1BgVA==xF35-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:23 +0200
[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 notadded.
* 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45ywACgkQjJF7f13FG6JJww/8DxaC2UOwxsNgFfOySZrifJglckkU1VWDZYCIqCHWssPxizqUIpIEcgZRZsrnqg/WNgUIps6ey6ZDDUefR3W5vna3jg+Rk+OJhSilSb1U6Y57kaI7r6CaaR/KHQWONkkcjcD1VPKejcTWd2yBNtPnM8eV+ZhW4rnYhvlvzoHKIFxHU9dh4TZGzQjQIoAz6M994/IA4ErkSEX2heTgGg+XStKc1kmLY0kjdbHl7dMqbTw3W9Nmyn3LAgtZ1DEYbucouQibp6J2gy05VYDHrYRasw9M2VnQ4uXBfr+jij/WLb1IxDsMK99ql3r0HCaiq/YEgamgvJvJFmpG8wk8qgHaJAQofgayVpOTiqzPbBNR12LvLD2GBh8LuKWT88REX+ERacuG1iSlnBo5v/QvGQQpDt/EEM+XxEH5HY3P7oS31Cz5eO3EJ94AatrjSHwULFSq9bUYinP7nuXNCaFHeJKZ0Ax0/sVHuArfWYOpGwSwkE5k+rKHQAltl+p57pUOXdVG02/7GKlFjvFYtEijo0SArCqeQV2dpdkOYiKusgudNdxU6oCsZf/gk81nt8EvssNoxCVlMppxlgVLLdYjNy69NzduTopznDJ3fy/FCDrocEJu7pmwDEtylKZ58cSAMRy/Ww+pLdTuRjPNHyKoSkBXMQVngTgMNj50zSxOlt2sMNg==R76u-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:24 +0200
[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, packagedindependently. This contains only what was needed for tla2tools, and sothere are parts of java-eclipse-lsp4j that are not packaged.
Note that this does not package the latest version (0.12.0 at the timeof writing)---it depends on the Xtend language, which is a hugepackaging effort. 0.10.0 is the version expected by tla2tools, forwhich 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB45zYACgkQjJF7f13FG6JAEA//eV53GBp6S7bqPZ5kA0dmkpVq1Emelixf70eI0jx2PPFrst5AF2MEGrs3VFt/s9f2wigofnxOgmP9F8zy5X2YX5YLHH+c8HtC6pjV7MSogbwMjLPFOwxFdV0iWLAPFWbI0PmGOSrrk4yVctFW27cbIq+SLNG/JRvFWw/P+QLoNM2OwTbg6Zo9EQWaEdaPvaBJpWHN+h0reC/jGBLxu13YlxQNmiVW9gCGBQUrLeNGHgCUlsb5pPCtpN+OWzCZpREdB3NRER4RzsO7CRewKnA4CPPAPTypxz3HpMsBc5mTsdy+LqA4f0+Dwh9YmkCCyAUW2t1BBXme/ejdUOJw2XIoTdatHJafYSi6biTtSqKcilo45h4To1kfb3JJTQprt/2/NBlbkdkL/RrLKotiLz9vtyz6iNNxSTqZluLOpipKDdt/JaWfKatRMKU62XznXFjqR6WBmulkHMgvgnqn1C9fzJb9Yq9L5pbVHtKv8lZqZN4UkmCOZi8W6AnEUZ+nGv4eDysMv0j14+HB6qWA9rOmfofMrTIKDCPSzWy7L3jUPQlhF4iQOZm0a/8Ml42yIFpEromEupxHYcWMOCEfuy7BT7QIsp93LYm+Neq4qXeXouMHoAC4FVPg/pC5kTPiC6ZKLACAQbWyJJgCrcAXAaaaaDOHdhYKOgIxTHccWN4MwBg==Pyst-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:24 +0200
[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 Javaknowledge, 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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB450IACgkQjJF7f13FG6KpFw//TSP3+7OiRKDJPMCYW5ZRlVGQUWDqpRmspbL9M9/Q522P6Ad7Ev/xvQbFeXf/NGPk6IKbqXKpDKAb/CFSLwoM7uoPfkuzwyQ9tZ85L4P1UOUPMVsupdE3wR1e8bc/FL3VOdX67veHtGYMVSyNa+D/jw6/jt6hmoMagVqglsxJP1v/EJmGIFSw57mZ3S38OaJxNH/aIsyCVGBzSU5SCgjY+vEiFYT5XbBnc48txRSdTi721Uk7wDsq0HH6zc46Qh51bFq9BIf47cAYL7S5ZUs6tLAAO6gjMlZBJ/uTRdUQyW6atJ4J8I9gAkgVJwMbYMI+oaBxjUD+MUOy20ytNM+dxIoBMd50eeoIA4pdwTug799gX31Vg/+RorqfSa/qlavEGlxDcOBiodt+JpMk6ZzMnvCOK+QPj88CCBGnoUseKkyCXhZmdooTGj0dQjiYAEinobp+/mq2C5pztqBqNGKHjCqGTEhrsR+p5NIzpNA2jP/ag4erQeG2m1LZs5khPKkBT8GvunuC1u+GyI08ftXjPHdan6IuAJRShDPlYrIp4pzFSTEcxYMFYxDDPva4DFlY6/M3c09ohRrkKL+K6r0LMhsqcjfRK8U/WsBP4uSOjgYTWUrfgD9GNYPJzybDVB/MGFJisuMpVDMzLePkNLKvGBtwDDCeWlq8q+afKPpP3V8==aWsF-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:24 +0200
[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.scmindex 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB4508ACgkQjJF7f13FG6KvfRAAu+GYZbT0gctMXpY7NYjTlrGWLDHq7KZAxMmUCOi775KqMn3wiXiOo1Yqaakbg4ffNK7Kt3vddNB9pl/8ZvMg2fVg3M9ixArJMfYelMgMNDdxLCkKcVi8otoZwAJQb7RXKDsjO4SiAAb+q5E7snMb0JdUmGF5IYiH5ZeVNmPG/Ic2eei5vF/tErtaq2fy2zak/oPQJtLXwfNIbpewTBNdrKqinj73G44D5FpSA4tgXZ4ZYAw38Jw05OXLgbeGG4ufi18gh2YJr2K3yepAQmUsVVbyso1XEkVNkyVDG8XdB7N85Eakqtqu3VbwOmlDHQ90u3NyihKPZHDYUsF/kW+8p+0ZQSCRO20mC6+7my4FYumIDsFMYpw7mgXg109ayDMEtkFagTDG6dPdPPeBHFShKGR9lCt8U5k85EL2nPvFe1O9VVKx/MhmoeFxnNsumo2ML4lliyfWccZ8R0D5szUxwYkCVEozD2IZpy5I1W52CV6k5pvxVVU5tWXZ+G3Egzs/Popa1OJkTiIpo/N+9H9gaXz6lQ7WXV+10dTPjlC0WHXoxHVzUJI/6MULrEeuXM4HXQr3poiKr3Pn4yYxkPjM+UHPGlFsI0YK6EBfY/U2AHjiXts46ZVgn5MJ8yg3uhYYdZ3cuvyHGMRgyitsQYkQOOm7FIPcscBjMGSycYnQzJU==eAie-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:24 +0200
[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 checkerand simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeXtypesetting system; PlusCal translator; and more. I have added fivewrapper scripts for convenience, rather than invoking `java' manually.The wrapper scripts are not comprehensive; users who are familiar withtla2tools.jar, or have read the book Specifying Systems, may stillinvoke the commands in the traditional way.
The minimum JDK version is 11. I chose to stick with that rather thanbumping 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 unnecessarydependencies.
Note that this is _not_ the TLA+ Toolbox, which is the GUI commonly usedwith 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.scmindex 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.patchnew file mode 100644index 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 GerwitzActivist For User Freedom | GNU Maintainer & VolunteerGPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05https://mikegerwitz.com
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB451sACgkQjJF7f13FG6ImbQ//UC9krmS4GYY1Bqd6yc0HOIMrUX1eL0SvZlPrA8kcbE/6XC2loAG7mrA+guFGD+KcR8Qzjnm4m6NYpREkb1AvKT3v37TzuPjKxAOvNYls5rYyA9CvxdguW9O+io2VkeeuJ97j4Sjtxiaxf0dpmDdAwtzKwUWMPUPatwbTYekA7ZZ1HW75FNpuHpQzhaoXmewD3YfBcQKwTceuGd2guvjl52SjCTfaOXBjtqotvGHgbte/63peVPv4f3G84jia39MHG7QDwrbA+nGjVkmmMhUYBzbrE+SrF8WIuovlg6MHLPpiErYjDcocalNSXCPcCum0BWxCeWLlk77EmAdjJLVXceDiPVAApfaQI68zY5jGLOqm8lVjLaLMGKfxlqKAYPvHAK4xeu+IDYwZFcrh/t68PljPuK3qt0YXg0n8T8U0MM1m+pModEKCcX+/rtv80wVOpGtaCZ4/i+NUy6C4N7nne0LXJ/6vgk78zTB61EsGviFMY95t5qM3YkVze0dpKnQ8/K9xL+4v0aGbWwausuks35VGFj21FOqpdprZU2FaAoNbn2Vc6Wlg0nPFD8vksv3dpZDxX8hnEq8ye19doA8YqFUNy7OpBAKNw7xiLTXVAZTRYfCxPoKkNqi/cHjg8E6U8BC4iws5xvrhKcs5gVwA5p8V76kR/VFbKtb1/seGVk4==1cqh-----END PGP SIGNATURE-----
M
M
Mike Gerwitz wrote on 16 Apr 03:29 +0200
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-----
iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB46JMACgkQjJF7f13FG6LEqxAAnt6ANYAatsKqb7oTHa/gv9rtqYO/cD4FNybCmS9+dk3cBeDJvOeaRfKkv3W26QPFejiFf8jfkL/yjaOmtYvjNSqmMAu6Jtxtkv18V/2nMVcMtSQaKUsMu2U7cGMJG46Zq85TTiVA8mv8D1jQ+kcmlIVUOdK2Ch4YqS9DNrt9+TloEeIm/ZhPbXMNaqorfEliob7SUzFV2kzl0RtGVZ3+Y8hI5zUgtDVEpAPc9WNdrkPGM1e1pjvYkP5Dt+pNeGQiTA0vF01LnUqAIZGdLjB2jJm/FfXg21F5p8pFTG8WMTjfw27mH5outklHpm/GvNz1k0Si3xbnH/IlEDfdJGmuSzX81RPOy1FUiCahTDRMw1m6pAMIL7lMU8LQQJKE95t7YpiyXvn4JhNgO9GosYjTW9R3y2Ys4ux57wIS3HCorNI8ouewy08yf1iNHL+yLdo9lG81B+aanmZSneos3Ov2BROC+AmBLj/dnksgIvAYPUITobU0nUCCUXz2D6VFAQGAjbQx5JuR6kFJoXOBO+pn9cuK4NrZ2yPDwRt7rljIFd+eV0YEyuVYKyUHtOZoTAyarPLHYLy5diM+Of/kocu31c/OWBiTZAGvv/077zIqHrA1zNDWhrc7FGnC21FVb8QIdevHRou9JUqCmY/6PfOeoWBPCz/MvKur4IV4tUt0HDM==JAyl-----END PGP SIGNATURE-----
L
L
Ludovic Courtès wrote on 5 May 17:02 +0200
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 asf30e8f29096e3ae2a4de689690daf5fa27a8c91b! \o/
For the tla2tools patch, I added the patch to gnu/local.mk. I also hadto 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 adifferent commit. Please take a look and let us know if anything’samiss.
Thanks for this heroic effort, and apologies for the delay!
Ludo’.
Closed
?