issues
search
tlaplus
/
tlapm
The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65
stars
20
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Syntax error when parameterized refinement occurs in subscript
#156
lemmy
opened
2 weeks ago
0
Use cmdliner in translate
#155
glondu
closed
2 weeks ago
0
Expose tlapm_lib for other projects.
#154
kape1395
opened
2 weeks ago
0
Add LSP command to add DEFs to a leaf proof for ExpandENABLED to work.
#153
kape1395
opened
3 weeks ago
2
Bump actions/download-artifact from 1 to 4.1.7 in /.github/workflows
#152
dependabot[bot]
closed
3 weeks ago
0
tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking
#151
lemmy
opened
1 month ago
2
Regression in BlockingQueue proof
#150
lemmy
opened
1 month ago
2
Add `make opam-deps-opt` to INSTALL.md
#149
lemmy
closed
1 month ago
0
Merge `updated_enabled_cdot`.
#148
kape1395
opened
1 month ago
2
Exposed parse method in TLAPM API
#147
ahelwer
closed
3 weeks ago
6
Intermittent build failures in CI
#146
ahelwer
closed
2 months ago
3
Add license field to opam package definition file
#145
ahelwer
closed
1 month ago
2
Emit bytecode in dune build for debugging
#144
ahelwer
closed
1 month ago
5
ENH: parse and expand bound tuples
#140
johnyf
opened
3 months ago
0
TLAPS proves `~(x = TRUE) <=> (x = FALSE)` in released versions
#139
lemmy
opened
3 months ago
3
Show ocaml version in https://github.com/tlaplus/tlapm/actions/workflows.
#138
lemmy
closed
3 months ago
0
Isabelle2020 dune m1
#137
lemmy
closed
3 months ago
3
Verify proofs in examples/ directory as part of PR workflow
#136
lemmy
opened
4 months ago
6
Make SimpleEventually proof a bit less simple.
#135
lemmy
opened
4 months ago
5
Rewrite Nat to {x ∈ Int : 0 ≤ x} instead of n ∈ Nat to (n ∈ Int ∧ 0 ≤ n).
#134
kape1395
closed
1 month ago
4
ISA: Example in `isabelle/examples/AtomicBakeryG.thy` fails.
#133
kape1395
closed
1 month ago
2
LSP: Make error position more precise in the case of incomplete expressions.
#132
kape1395
opened
4 months ago
0
Isabelle202X cleanup
#131
kape1395
closed
1 month ago
3
TLAPM Error
#130
mery54
closed
4 months ago
1
LSP: Only show "RECURSIVE unsupported" warnings if the module contains proofs.
#129
kape1395
opened
4 months ago
0
LSP: Some errors are shown on wrong files.
#128
kape1395
opened
5 months ago
0
Request: add my SSH public keys to the set of authorized keys on the INRIA server
#127
ahelwer
closed
5 months ago
14
Added Arch Linux instructions to INSTALL.md
#126
ahelwer
closed
5 months ago
0
Update the installation instructions.
#125
kape1395
closed
5 months ago
18
Try use Isabelle2024-RC2.
#124
kape1395
closed
4 months ago
16
Binary installer links on the TLAPS website are broken
#123
uguryavuz
closed
5 months ago
0
Download of the TLAPS tar.gz file is missing Zenon, Isabelle and emacs, while TLAPM is downloaded
#122
fowlerlee
closed
7 months ago
4
useless quantifier prevents new SMT from proving obligation
#121
damiendoligez
opened
7 months ago
0
Variable renames in LAMBDA
#120
kape1395
opened
7 months ago
3
Module references considered differently SANY and TLAPM
#119
kape1395
opened
7 months ago
7
Why the standard modules can be overriden?
#118
kape1395
closed
7 months ago
4
Mark release 202210041448 as latest
#117
ahelwer
closed
8 months ago
3
Make it compile on OCaml 5.1.
#116
kape1395
closed
7 months ago
1
Use HTTPS to download the Isabelle.
#115
kape1395
closed
8 months ago
1
LSP: Some proof steps are shown twice.
#114
kape1395
closed
8 months ago
1
LSP: Show proved/pending/failed step count in the decorator comment of a structured proof step.
#113
kape1395
closed
8 months ago
1
LSP: WITNESS is not shown as a step.
#112
kape1395
closed
8 months ago
1
TLAPM should provide better error message if a recursive operator is enounted.
#111
kape1395
closed
8 months ago
1
fix laziness in t_hyps.ml
#110
damiendoligez
closed
8 months ago
0
Use Isabelle202x
#109
kape1395
closed
1 month ago
33
LSP: Re-read proof states of all the obligations after an edit
#108
kape1395
closed
8 months ago
1
LSP: Retain the last fail state of an obligation.
#107
kape1395
closed
9 months ago
1
LSP: The TLAPM parser often does not provide an error position.
#106
kape1395
closed
1 month ago
4
LSP: Progress report is sometimes off.
#105
kape1395
closed
8 months ago
1
LSP: Buffer decorations before sending them to the IDE.
#104
kape1395
closed
9 months ago
1
Next