Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / tlaplus/tlapm issues and pull requests

#176 - change magic number for fingerprint files

Pull Request - State: open - Opened by damiendoligez 12 days ago - 1 comment

#175 - Cancel CI workflow if new changes are pushed

Pull Request - State: closed - Opened by ahelwer 20 days ago

#173 - TLAPM fails to parse decimal numbers of form `.12345` without leading zero

Issue - State: open - Opened by ahelwer 26 days ago
Labels: bug, syntax parser

#172 - TLAPM incorrectly accepts some unit-level definitions prefixed by `LOCAL`

Issue - State: open - Opened by ahelwer 26 days ago
Labels: bug, syntax parser

#171 - Functions.tla and SequencesExt.tla out-of-sync with CommunityModules

Issue - State: open - Opened by lemmy 27 days ago
Labels: bug

#170 - TLAPM parser does not accept implicit `<*>`/`<+>` proof step IDs with names

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#169 - TLAPM parser accepts incorrect use of labels that break operator precedence

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#168 - TLAPM parser accepts invalid use of parentheses to escape conjunction list

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#167 - TLAPM parser does not accept `INSTANCE` proof step type

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#167 - TLAPM parser does not accept `INSTANCE` proof step type

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#166 - TLAPM parser does not accept `MODULE` references in several places

Issue - State: open - Opened by ahelwer about 1 month ago - 1 comment
Labels: bug, syntax parser

#165 - TLAPM parser does not accept proof step references in `QED BY` with implicit `<*>` proof level

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#165 - TLAPM parser does not accept proof step references in `QED BY` with implicit `<*>` proof level

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#164 - TLAPM fails to parse set literals containing multiple expressions of form `x \in S`

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#164 - TLAPM fails to parse set literals containing multiple expressions of form `x \in S`

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#163 - TLAPM syntax parser does not support bitfield number formats

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#163 - TLAPM syntax parser does not support bitfield number formats

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#162 - TLAPM syntax parser treats Cartesian products differently from infix operators

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#162 - TLAPM syntax parser treats Cartesian products differently from infix operators

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#161 - TLAPM syntax parser does not accept prefix operators as higher-level operator parameters

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#161 - TLAPM syntax parser does not accept prefix operators as higher-level operator parameters

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#160 - TLAPM does not parse quantifiers using `\forall` or `\exists` keywords instead of `\A` or `\E`

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#160 - TLAPM does not parse quantifiers using `\forall` or `\exists` keywords instead of `\A` or `\E`

Issue - State: open - Opened by ahelwer about 1 month ago
Labels: bug, syntax parser

#159 - Run corpus of TLA+ syntax tests in simple pass/fail manner

Pull Request - State: closed - Opened by ahelwer about 1 month ago - 1 comment

#158 - Pin dependency versions for dune build

Issue - State: open - Opened by ahelwer about 1 month ago - 6 comments

#157 - Proof for ENABLED TRUE fails

Issue - State: closed - Opened by jspenger about 1 month ago - 1 comment

#156 - Syntax error when parameterized refinement occurs in subscript

Issue - State: open - Opened by lemmy 2 months ago - 1 comment
Labels: bug, syntax parser

#155 - Use cmdliner in translate

Pull Request - State: closed - Opened by glondu 2 months ago

#155 - Use cmdliner in translate

Pull Request - State: closed - Opened by glondu 2 months ago

#154 - Expose tlapm_lib for other projects.

Pull Request - State: open - Opened by kape1395 2 months ago

#154 - Expose tlapm_lib for other projects.

Pull Request - State: open - Opened by kape1395 2 months ago

#153 - Add LSP command to add DEFs to a leaf proof for ExpandENABLED to work.

Issue - State: open - Opened by kape1395 2 months ago - 2 comments
Labels: enhancement

#153 - Add LSP command to add DEFs to a leaf proof for ExpandENABLED to work.

Issue - State: open - Opened by kape1395 2 months ago - 2 comments
Labels: enhancement

#152 - Bump actions/download-artifact from 1 to 4.1.7 in /.github/workflows

Pull Request - State: closed - Opened by dependabot[bot] 3 months ago
Labels: dependencies

#152 - Bump actions/download-artifact from 1 to 4.1.7 in /.github/workflows

Pull Request - State: closed - Opened by dependabot[bot] 3 months ago
Labels: dependencies

#151 - tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking

Issue - State: open - Opened by lemmy 3 months ago - 4 comments
Labels: bug

#150 - Regression in BlockingQueue proof

Issue - State: open - Opened by lemmy 3 months ago - 2 comments

#150 - Regression in BlockingQueue proof

Issue - State: open - Opened by lemmy 3 months ago - 2 comments

#149 - Add `make opam-deps-opt` to INSTALL.md

Pull Request - State: closed - Opened by lemmy 3 months ago

#148 - Merge `updated_enabled_cdot`.

Pull Request - State: open - Opened by kape1395 3 months ago - 2 comments

#148 - Merge `updated_enabled_cdot`.

Pull Request - State: open - Opened by kape1395 3 months ago - 2 comments

#147 - Exposed parse method in TLAPM API

Pull Request - State: closed - Opened by ahelwer 3 months ago - 6 comments

#147 - Exposed parse method in TLAPM API

Pull Request - State: closed - Opened by ahelwer 3 months ago - 6 comments

#146 - Intermittent build failures in CI

Issue - State: closed - Opened by ahelwer 4 months ago - 3 comments

#146 - Intermittent build failures in CI

Issue - State: closed - Opened by ahelwer 4 months ago - 3 comments

#145 - Add license field to opam package definition file

Pull Request - State: closed - Opened by ahelwer 4 months ago - 2 comments

#145 - Add license field to opam package definition file

Pull Request - State: closed - Opened by ahelwer 4 months ago - 2 comments

#144 - Emit bytecode in dune build for debugging

Pull Request - State: closed - Opened by ahelwer 4 months ago - 5 comments

#144 - Emit bytecode in dune build for debugging

Pull Request - State: closed - Opened by ahelwer 4 months ago - 5 comments

#140 - ENH: parse and expand bound tuples

Pull Request - State: open - Opened by johnyf 5 months ago - 7 comments

#139 - TLAPS proves `~(x = TRUE) <=> (x = FALSE)` in released versions

Issue - State: open - Opened by lemmy 6 months ago - 3 comments
Labels: bug

#138 - Show ocaml version in https://github.com/tlaplus/tlapm/actions/workflows.

Pull Request - State: closed - Opened by lemmy 6 months ago
Labels: enhancement

#137 - Isabelle2020 dune m1

Pull Request - State: closed - Opened by lemmy 6 months ago - 3 comments
Labels: enhancement

#137 - Isabelle2020 dune m1

Pull Request - State: closed - Opened by lemmy 6 months ago - 3 comments
Labels: enhancement

#136 - Verify proofs in examples/ directory as part of PR workflow

Issue - State: open - Opened by lemmy 6 months ago - 6 comments
Labels: enhancement, testing

#136 - Verify proofs in examples/ directory as part of PR workflow

Issue - State: open - Opened by lemmy 6 months ago - 6 comments
Labels: enhancement, testing

#135 - Make SimpleEventually proof a bit less simple.

Pull Request - State: open - Opened by lemmy 6 months ago - 5 comments
Labels: enhancement, documentation

#134 - Rewrite Nat to {x ∈ Int : 0 ≤ x} instead of n ∈ Nat to (n ∈ Int ∧ 0 ≤ n).

Pull Request - State: closed - Opened by kape1395 6 months ago - 4 comments

#134 - Rewrite Nat to {x ∈ Int : 0 ≤ x} instead of n ∈ Nat to (n ∈ Int ∧ 0 ≤ n).

Pull Request - State: closed - Opened by kape1395 6 months ago - 4 comments

#133 - ISA: Example in `isabelle/examples/AtomicBakeryG.thy` fails.

Issue - State: closed - Opened by kape1395 6 months ago - 2 comments

#133 - ISA: Example in `isabelle/examples/AtomicBakeryG.thy` fails.

Issue - State: closed - Opened by kape1395 6 months ago - 2 comments

#131 - Isabelle202X cleanup

Pull Request - State: closed - Opened by kape1395 6 months ago - 3 comments

#131 - Isabelle202X cleanup

Pull Request - State: closed - Opened by kape1395 6 months ago - 3 comments

#130 - TLAPM Error

Issue - State: closed - Opened by mery54 6 months ago - 1 comment

#128 - LSP: Some errors are shown on wrong files.

Issue - State: open - Opened by kape1395 7 months ago

#126 - Added Arch Linux instructions to INSTALL.md

Pull Request - State: closed - Opened by ahelwer 7 months ago

#125 - Update the installation instructions.

Pull Request - State: closed - Opened by kape1395 7 months ago - 18 comments

#125 - Update the installation instructions.

Pull Request - State: closed - Opened by kape1395 7 months ago - 18 comments

#124 - Try use Isabelle2024-RC2.

Pull Request - State: closed - Opened by kape1395 7 months ago - 16 comments

#124 - Try use Isabelle2024-RC2.

Pull Request - State: closed - Opened by kape1395 7 months ago - 16 comments

#123 - Binary installer links on the TLAPS website are broken

Issue - State: closed - Opened by uguryavuz 8 months ago

#120 - Variable renames in LAMBDA

Issue - State: open - Opened by kape1395 9 months ago - 3 comments
Labels: bug, translator

#120 - Variable renames in LAMBDA

Issue - State: open - Opened by kape1395 9 months ago - 3 comments
Labels: bug, translator

#119 - Module references considered differently SANY and TLAPM

Issue - State: open - Opened by kape1395 10 months ago - 7 comments
Labels: bug, semantic checker

#119 - Module references considered differently SANY and TLAPM

Issue - State: open - Opened by kape1395 10 months ago - 7 comments
Labels: bug, semantic checker

#109 - Use Isabelle202x

Pull Request - State: closed - Opened by kape1395 11 months ago - 33 comments

#109 - Use Isabelle202x

Pull Request - State: closed - Opened by kape1395 11 months ago - 33 comments

#106 - LSP: The TLAPM parser often does not provide an error position.

Issue - State: closed - Opened by kape1395 12 months ago - 4 comments

#101 - Give Karolis write access to the repo

Issue - State: closed - Opened by ahelwer 12 months ago - 5 comments

#100 - LSP server fails with empty document.

Issue - State: closed - Opened by kape1395 about 1 year ago - 1 comment

#99 - fix install location for ptl_to_trp

Pull Request - State: closed - Opened by damiendoligez about 1 year ago

#98 - fixed bogus proof in setEuclid_test.tla

Pull Request - State: closed - Opened by muenchnerkindl about 1 year ago - 2 comments

#97 - Unable to compile on M1 Mac

Issue - State: closed - Opened by uguryavuz about 1 year ago - 14 comments

#96 - Unify pr/main workflows and use tlaplus/examples as integration tests

Pull Request - State: closed - Opened by ahelwer about 1 year ago - 26 comments

#95 - Branch `updated_enabled_cdot` on top of dune, ocaml-5 and lsp.

Pull Request - State: closed - Opened by kape1395 about 1 year ago - 1 comment

#94 - QED step has no locus assigned.

Issue - State: closed - Opened by kape1395 about 1 year ago - 2 comments

#93 - Language Server Protocol for TLAPM

Pull Request - State: closed - Opened by kape1395 about 1 year ago - 14 comments

#92 - Introduce a `develop` branch?

Issue - State: closed - Opened by kape1395 about 1 year ago - 12 comments

#91 - OCaml 5.1

Pull Request - State: closed - Opened by kape1395 about 1 year ago

#90 - LSP support

Issue - State: closed - Opened by kape1395 about 1 year ago - 4 comments

#89 - Inconsistent verification of TLAPS proofs

Issue - State: open - Opened by uguryavuz over 1 year ago
Labels: bug

#88 - Nondeterministic tlapm install failure on ubuntu (building Pure failed)

Issue - State: closed - Opened by ahelwer over 1 year ago - 4 comments

#87 - Support dune build deps macos (vipo)

Pull Request - State: closed - Opened by vipo over 1 year ago

#85 - Fingerprints seemingly ignored for some proofs

Issue - State: closed - Opened by ahelwer over 1 year ago - 5 comments

#84 - fix disappearing fingerprints

Pull Request - State: closed - Opened by damiendoligez over 1 year ago