Shon Feder

[FEATURE] Package for ubuntu

1

Towards #159

[FEATURE] Deploy the latest stable version of the docs separately

2

As a followup to #400, we should also build and deploy and unstable version of the documentation. (At some future point, we'll want to keep different versions of the manual...

Add link checking to mdBook rendering

1

See https://crates.io/crates/mdbook-linkcheck

[FEATURE] Report name of operators and arguments that faile to type check

1

Currently, type check failures on operators just give the operator signature and the types of the arguments that cause the checking failure. E.g., ``` [TwoPhase.tla:68:6-68:21]: No match between operator signature...

[FEATURE] Improve error messages around type annotations

1

- [ ] Missing annotations on VARIABLE's don't include line numbers: ``` PASS #1: TypeCheckerSnowcat I@08:18:53.210 > Running Snowcat .::. I@08:18:53.210 Typing input error: Expected a type annotation for VARIABLE...

[FEATURE] Overhaul error message treatment

6

During our retro last week, we discussed some ways we could change the error messaging and user-error handling that would improve learnability and user feedback, and perhaps even improve our...

[BUG] Invalid CLI arguments lead to unhandled exception:

1

MWE: ``` check --algo=asdoinasdf $PWD/test/tla/letpoly_inst.tla ... java.lang.IllegalArgumentException: Unexpected checker.algo=asdoinasdf at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:108) at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22) at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37) at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:188) at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95) at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:323) at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95) at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45) at at.forsyte.apalache.tla.Tool.main(Tool.scala) ``` We should...

[wish] Put the "L" in "REPL" by making it loop

1

The current behavior of the repl is to read an expression, query the goal, and quit. It would be much nicer if it looped, and allowed posing repeated queries :)...

Instruct user on remedy when credentials become invalidated

4

I received ``` dune-release: [ERROR] Could not retrieve release ID from response, unexpected Github API error: "Bad credentials" ``` due to a revoked token that was cached long ago. There...

dune-release: [ERROR] Could not retrieve release ID from response, unexpected Github API error: "Not Found"

9

I'm receiving the titular error on version 1.4.0 and ``` uname -a Linux comp 5.4.89-1-MANJARO #1 SMP PREEMPT Tue Jan 12 23:39:44 UTC 2021 x86_64 GNU/Linux ``` ``` [sf@comp emojitsu]$...