From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:4a6f::]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id LrSfJyLBd2Bo3gAAgWs5BA (envelope-from ) for ; Thu, 15 Apr 2021 06:29:22 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id aILuHCLBd2B0QgAAB5/wlQ (envelope-from ) for ; Thu, 15 Apr 2021 04:29:22 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id EC9F717374 for ; Thu, 15 Apr 2021 06:29:21 +0200 (CEST) Received: from localhost ([::1]:53414 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lWtd3-0000cW-0W for larch@yhetil.org; Thu, 15 Apr 2021 00:29:21 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:58222) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lWtcm-0000aP-Lc for guix-patches@gnu.org; Thu, 15 Apr 2021 00:29:04 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:52919) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lWtcm-0001mB-ES for guix-patches@gnu.org; Thu, 15 Apr 2021 00:29:04 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lWtcm-0007is-As for guix-patches@gnu.org; Thu, 15 Apr 2021 00:29:04 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#47789] [PATCH 6/6] gnu: Add tla2tools. Resent-From: Mike Gerwitz Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 15 Apr 2021 04:29:04 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 47789 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 47789@debbugs.gnu.org Received: via spool by 47789-submit@debbugs.gnu.org id=B47789.161846094329679 (code B ref 47789); Thu, 15 Apr 2021 04:29:04 +0000 Received: (at 47789) by debbugs.gnu.org; 15 Apr 2021 04:29:03 +0000 Received: from localhost ([127.0.0.1]:36229 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lWtck-0007iO-Va for submit@debbugs.gnu.org; Thu, 15 Apr 2021 00:29:03 -0400 Received: from eggs.gnu.org ([209.51.188.92]:45568) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lWtci-0007hL-Oj for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 00:29:01 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:57389) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lWtcd-0001e4-Jl for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 00:28:55 -0400 Received: from localhost ([::1]:48864 helo=mikegerwitz-pc) by fencepost.gnu.org with esmtps (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1lWtcc-0006Q3-FO for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 00:28:55 -0400 From: Mike Gerwitz In-Reply-To: Date: Thu, 15 Apr 2021 00:27:27 -0400 References: User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) X-From-Line: fc94440ebc83044f49813f58633ccaa6b1becc65 Mon Sep 17 00:00:00 2001 Message-Id: MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1618460962; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post; bh=TaDcZVjT81gBTSRH5N1+jMy/2thV2DyBgHEJQ6i42Ic=; b=kQyAJCfGo99HCxXFfFnA3ogUMvbU0KHl80aP+aFJRSZbOywhEd6rfYUcL8WpNzFhNWDnz3 GuCdEPnZzJ6MoMsIGdtjCWrLQpoKFN0Rxl8D3tqfZd4P1WjbNFGnedsMKxYj/YCC34L5Ez znimw6+PN7QFRobBycWQTcL04eQiDAxOzJ6DzXBIuxkSubRCch0lAb1ncD1hAB8rVNNvXR uO2Szyr1IkXlrRZ7R0X3v3qT7Xg7l0obDTPdwKK6/t6HdYUfu5PiqzuKqxNNt+bTgfn3Nw Su2iX1+aUBdNgQyBizLP0Ghuq43qBBvKgtrg6F3nsxiPpsOkk44fm+XJDbvjow== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1618460962; a=rsa-sha256; cv=none; b=DizVNvio4lm7cP1c+cNlkwb7jM6+QnJJ8JUQrR7Kpdg17LELY15ZD9bVdGXWcimqm86vER pbY7oWWySp1uxoEyYsOYccNCRFrKi/SJijVtIPvLALg1Kl/klVZvHvLmWU99kP+pobbWa5 hR36loW1caiKlZyf6xORSNmtIWrq/NQtvUbgIxOWWBcV6m/L1iyfMIhhVPjEKTRZrcIJPR wSfpJ42OXDQEmmqBvbCdVpJl0I+clY9M4BL97S2JdswF9l8vCDs1V56Ku6yyfRUQyM+W1o wRbAKvjZVucIqEUxlm5Mpq79u7/KSntO2TZOwoSoO5onklDqgaN3K/9prSoMNA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; dmarc=pass (policy=none) header.from=gnu.org; spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: -0.04 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=pass (policy=none) header.from=gnu.org; spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: EC9F717374 X-Spam-Score: -0.04 X-Migadu-Scanner: scn0.migadu.com X-TUID: ZpMWgZ9us/fb --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable 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. =2D-- 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 diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm index 4d6befe511..087f411258 100644 =2D-- a/gnu/packages/java.scm +++ b/gnu/packages/java.scm @@ -14040,3 +14040,137 @@ can be interpreted by IDEs and static analysis to= ols 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-termi= nal") + ("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.propert= ies + (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 comm= on + ;; commands within tla2tools.jar. Users can still invo= ke + ;; 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-d= ebug) + ("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 i= dea +that the best way to describe things precisely is with simple +mathematics. TLA+ and its tools are useful for eliminating fundamental de= sign +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 =2D-- /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' targe= t. +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 @@ + + +=20 ++ ++ ++ ++ ++ ++ ++ ++ ++ ++ ++ + + + +@@ -217,17 +228,7 @@ + + + +- +- +- +- +- +- +- +- +- +- +- ++ + + + +@@ -259,17 +260,7 @@ + + + +- +- +- +- +- +- +- +- +- +- +- ++ + +=20 + +@@ -373,14 +364,8 @@ + src/tla2sany/parser/Token.09-09-07, + src/tla2sany/parser/TokenMgrError.09-09-07"/> + +- +- +- +- +- +- + +- ++ + + + +@@ -389,14 +374,8 @@ + =20 + +- + +- +- +- +- + + + =2D-=20 Mike Gerwitz Activist For User Freedom | GNU Maintainer & Volunteer GPG: D6E9 B930 028A 6C38 F43B 2388 FEF6 3574 5E6F 6D05 https://mikegerwitz.com --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----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----- --=-=-=--