Thanks for the link to the nightly builds. I would like to ask if you know when this change might make it into an "official" release (I put that in quotes as I am not familiar with the TLA+ release approach, rhythms, etc.)
I think we might need to look to the next release for various traceability reasons.
On Wednesday, November 18, 2020 at 1:25:16 AM UTC-5 Chuck Lutz wrote:
Hi again,
Wow, thanks very much for the quick update!
Regards,
Chuck
On Tuesday, November 17, 2020 at 11:14:43 AM UTC-5 Markus Alexander Kuppe wrote:
On 17.11.20 07:27, Chuck Lutz wrote:
>
> Yes, correct - the HeapSort was specifically the problem.
>
> As I was not too specific before :-), here is the main bit:
>
> "HeapSortAlgorithm.java 1.0 95/06/23 Jason Harrison
> Copyright (c) 1995 University of British Columbia"
>
> Would omitting only this file disable TLC or anything vital? It seemed
> that this is perhaps part of a layout algorithm for translating to TeX,
> so I assumed that would be a "nice to have" vs. part of the core
> functionality.
Hi Chuck,
the implementation of HeapSort has been removed [1]. You can download
new builds of TLC and the Toolbox from [2]. Omitting the file would
indeed break the pretty-printer (TeX).
Markus
[1]
https://github.com/tlaplus/tlaplus/commit/8b52d238eb9f17df98dd795dbb589d9fba4a5822
[2] https://nightly.tlapl.us