From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:8:6d80::]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id oJ4YOmLoeGB9UQEAgWs5BA (envelope-from ) for ; Fri, 16 Apr 2021 03:29:06 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id kISiNGLoeGBDHgAAbx9fmQ (envelope-from ) for ; Fri, 16 Apr 2021 01:29:06 +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 6746C18C4E for ; Fri, 16 Apr 2021 03:29:04 +0200 (CEST) Received: from localhost ([::1]:45030 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lXDI7-0006nZ-KD for larch@yhetil.org; Thu, 15 Apr 2021 21:29:03 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:52186) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lXDH8-0006Kz-QD for guix-patches@gnu.org; Thu, 15 Apr 2021 21:28:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:56346) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lXDH8-0003dN-90 for guix-patches@gnu.org; Thu, 15 Apr 2021 21:28:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lXDH8-0008Tu-64 for guix-patches@gnu.org; Thu, 15 Apr 2021 21:28:02 -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: Fri, 16 Apr 2021 01:28:02 +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.161853644232543 (code B ref 47789); Fri, 16 Apr 2021 01:28:02 +0000 Received: (at 47789) by debbugs.gnu.org; 16 Apr 2021 01:27:22 +0000 Received: from localhost ([127.0.0.1]:39657 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lXDGT-0008Sj-8N for submit@debbugs.gnu.org; Thu, 15 Apr 2021 21:27:22 -0400 Received: from eggs.gnu.org ([209.51.188.92]:39272) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lXDGG-0008Rj-8s for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 21:27:09 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:47793) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lXDG9-0003IE-V3 for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 21:27:02 -0400 Received: from localhost ([::1]:39263 helo=mikegerwitz-pc) by fencepost.gnu.org with esmtps (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1lXDG8-0000ln-MY for 47789@debbugs.gnu.org; Thu, 15 Apr 2021 21:27:01 -0400 From: Mike Gerwitz In-Reply-To: Date: Thu, 15 Apr 2021 21:24:39 -0400 References: User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) X-From-Line: ebb4608d38a42da2076671603682f3e35ab53ebf 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=1618536544; 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=4a78UBkNw1ZEEXLqiCLZpL47gXt7ee1aQmKZ8wzuqH4=; b=KdAt89H1Z3Ilw4VuiwJTLQhLDrGik007HOgR1QjOl6sw9CdzXFSwTqNyCe4qTYs+0A1sBW ALZgh/xaGZarZsc6WGDVtgrY1S9kuxns5EpUNYzDiMzjXpLRcySBNa0HrF1lx1aRSUTxbw kWx3AKwkCP4ICCsG4jMZsqbE6o6B7TtLNv58zteIMuQH/fZM3SNIullz3FDvZnrnmSQPFY 4q4pMZVPnyQKPqTBewzxExpqb0vJ8p8RuJyImHZiFBxFe99TiXcvk0eTLb7tkBw3pxAwD7 GOF4MAO5TQXqPmw+kDLd/a9dGrpiueSiFPlNuvY9gTlnvB0CkexpiJ3jO/krVw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1618536544; a=rsa-sha256; cv=none; b=JLZdZrWiwjeNq+tiTLgI4Z7006mlAFUbNkLBOmubyWXZaXeiawSe3b5hI4+JDW3+zP2chb GTHalq9y6duX/FoYggh1NNW9PjQd31cMiwbAjhmAbjgzrW+Vgt781VH2TdWOuS3Td/AWI7 M+GPHq2MIdLRKZeMv915ff3rzi46k1WCUSHp7/V3ZZPKtj2Q0vEAum6MPqZ66jMNAUg7Qz gB00k63lmnapEYiOryXK9ANLc1pEVSQDLtjVEu0Ofb+TiPDhncW+LW2PuORWpzVC87mwof +4l3r+1uSvdHw8+zZ0nTxYHPEQvKKT3Hjrx/sRtXB3pcqIaP0GOOjHTa1ndMgQ== 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: -1.54 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: 6746C18C4E X-Spam-Score: -1.54 X-Migadu-Scanner: scn0.migadu.com X-TUID: Vr6KJ+URzNZ7 --=-=-= 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 | 132 ++++++++++++++++++ .../patches/tla2tools-build-xml.patch | 109 +++++++++++++++ 2 files changed, 241 insertions(+) create mode 100644 gnu/packages/patches/tla2tools-build-xml.patch diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm index a474c40ebb..12e3577ca4 100644 =2D-- a/gnu/packages/java.scm +++ b/gnu/packages/java.scm @@ -14028,3 +14028,135 @@ 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$")))))) + (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)))) + (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.propert= ies + (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 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 + "#!/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-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----- iQIzBAEBCgAdFiEEtyLNo03iHAANpWtgjJF7f13FG6IFAmB451sACgkQjJF7f13F G6ImbQ//UC9krmS4GYY1Bqd6yc0HOIMrUX1eL0SvZlPrA8kcbE/6XC2loAG7mrA+ guFGD+KcR8Qzjnm4m6NYpREkb1AvKT3v37TzuPjKxAOvNYls5rYyA9CvxdguW9O+ io2VkeeuJ97j4Sjtxiaxf0dpmDdAwtzKwUWMPUPatwbTYekA7ZZ1HW75FNpuHpQz haoXmewD3YfBcQKwTceuGd2guvjl52SjCTfaOXBjtqotvGHgbte/63peVPv4f3G8 4jia39MHG7QDwrbA+nGjVkmmMhUYBzbrE+SrF8WIuovlg6MHLPpiErYjDcocalNS XCPcCum0BWxCeWLlk77EmAdjJLVXceDiPVAApfaQI68zY5jGLOqm8lVjLaLMGKfx lqKAYPvHAK4xeu+IDYwZFcrh/t68PljPuK3qt0YXg0n8T8U0MM1m+pModEKCcX+/ rtv80wVOpGtaCZ4/i+NUy6C4N7nne0LXJ/6vgk78zTB61EsGviFMY95t5qM3YkVz e0dpKnQ8/K9xL+4v0aGbWwausuks35VGFj21FOqpdprZU2FaAoNbn2Vc6Wlg0nPF D8vksv3dpZDxX8hnEq8ye19doA8YqFUNy7OpBAKNw7xiLTXVAZTRYfCxPoKkNqi/ cHjg8E6U8BC4iws5xvrhKcs5gVwA5p8V76kR/VFbKtb1/seGVk4= =1cqh -----END PGP SIGNATURE----- --=-=-=--