From patchwork Thu Apr 15 04:22:03 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Mike Gerwitz X-Patchwork-Id: 71 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 0A07727BC76; Thu, 15 Apr 2021 05:25:17 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI, RCVD_IN_MSPIKE_H4,RCVD_IN_MSPIKE_WL,SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 2CE2327BC77 for ; Thu, 15 Apr 2021 05:25:14 +0100 (BST) Received: from localhost ([::1]:52962 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lWtY5-0008IX-6g for patchwork@mira.cbaines.net; Thu, 15 Apr 2021 00:24:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:57458) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lWtXu-0008FL-FU for guix-patches@gnu.org; Thu, 15 Apr 2021 00:24:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:52894) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lWtXu-0006mn-7t for guix-patches@gnu.org; Thu, 15 Apr 2021 00:24:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lWtXu-0007Zl-4G for guix-patches@gnu.org; Thu, 15 Apr 2021 00:24:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#47789] [PATCH 0/6] Add TLA+ Tools (tla2tools) Resent-From: Mike Gerwitz Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 15 Apr 2021 04:24:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 47789 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 47789@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.161846059829067 (code B ref -1); Thu, 15 Apr 2021 04:24:01 +0000 Received: (at submit) by debbugs.gnu.org; 15 Apr 2021 04:23:18 +0000 Received: from localhost ([127.0.0.1]:36207 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lWtXC-0007Yl-HC for submit@debbugs.gnu.org; Thu, 15 Apr 2021 00:23:18 -0400 Received: from lists.gnu.org ([209.51.188.17]:54566) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lWtXB-0007Ye-1B for submit@debbugs.gnu.org; Thu, 15 Apr 2021 00:23:17 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:57386) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lWtXA-000890-Qs for guix-patches@gnu.org; Thu, 15 Apr 2021 00:23:16 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:57324) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lWtXA-0006Kd-Js for guix-patches@gnu.org; Thu, 15 Apr 2021 00:23:16 -0400 Received: from localhost ([::1]:48798 helo=mikegerwitz-pc) by fencepost.gnu.org with esmtps (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1lWtXA-0002bR-2O for guix-patches@gnu.org; Thu, 15 Apr 2021 00:23:16 -0400 From: Mike Gerwitz Date: Thu, 15 Apr 2021 00:22:03 -0400 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 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches This introduces tla2tools.jar, which contains the TLA+ model checker and simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeX typesetting system; PlusCal translator; and more. I have added five wrapper scripts for convenience, rather than invoking `java' manually. The wrapper scripts are not comprehensive; users who are familiar with tla2tools.jar, or have read the book Specifying Systems, may still invoke the commands in the traditional way. This was significnatly more involved than I had anticipated, and I was forced to make some compromises on how I handled dependencies. Most notably, rather than packaging the entirety of LSP4J and JLine 3, I packaged only what tla2tools used, since going all the way would have been a significant undertaking that I would not have been able to see through. I have not packaged Java libraries for Guix before (and it's been years since I packaged anything else), so please be critical and let me know what I can do better. I hope to explore packaging TLAPS next. I don't anticipate packaging the Toolbox for Guix, which is TLA+'s GUI; there are a huge number of dependencies. Enjoy! Mike Gerwitz (6): gnu: Add java-gson-2.8.6. gnu: Add java-eclipse-xtext-xbase-lib. gnu: Add java-eclipse-lsp4j packages. gnu: Add java-jline-terminal. gnu: Add java-jline-reader. gnu: Add tla2tools. gnu/packages/java.scm | 410 ++++++++++++++++++ .../patches/tla2tools-build-xml.patch | 109 +++++ 2 files changed, 519 insertions(+) create mode 100644 gnu/packages/patches/tla2tools-build-xml.patch