GNU bug report logs - #47789
[PATCH 0/6] Add TLA+ Tools (tla2tools)

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Mike Gerwitz <mtg <at> gnu.org>
Subject: bug#47789: closed (Re: bug#47789: [PATCH 0/6] Add TLA+ Tools
 (tla2tools))
Date: Wed, 05 May 2021 15:04:02 +0000

[Message part 1 (text/plain, inline)]

Your bug report

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

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 47789 <at> debbugs.gnu.org.

-- 
47789: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=47789
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: Ludovic Courtès <ludo <at> gnu.org>
To: Mike Gerwitz <mtg <at> gnu.org>
Cc: 47789-done <at> debbugs.gnu.org
Subject: Re: bug#47789: [PATCH 0/6] Add TLA+ Tools (tla2tools)
Date: Wed, 05 May 2021 17:02:30 +0200

Hi Mike,

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

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

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

Ludo’.

[Message part 3 (message/rfc822, inline)]

From: Mike Gerwitz <mtg <at> gnu.org>
To: guix-patches <at> gnu.org
Subject: [PATCH 0/6] Add TLA+ Tools (tla2tools)
Date: Thu, 15 Apr 2021 00:22:03 -0400

[Message part 4 (text/plain, inline)]

This introduces tla2tools.jar, which contains the TLA+ model checker
and simulator (TLC); a TLA+ REPL; a semantic analyzer (SANY); the TLATeX
typesetting system; PlusCal translator; and more.  I have added five
wrapper scripts for convenience, rather than invoking `java' manually.
The wrapper scripts are not comprehensive; users who are familiar with
tla2tools.jar, or have read the book Specifying Systems, may still
invoke the commands in the traditional way.

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

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

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

Enjoy!

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

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

-- 
Mike Gerwitz
Activist For User Freedom | GNU Maintainer & Volunteer
GPG: D6E9 B930 028A 6C38 F43B  2388 FEF6 3574 5E6F 6D05
https://mikegerwitz.com

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.