Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
lemmy opened this issue Oct 28, 2024 · 0 comments
Open

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

lemmy opened this issue Oct 28, 2024 · 0 comments
Labels
bug An error, usually in the code.

Comments

@lemmy
Copy link
Member

lemmy commented Oct 28, 2024

The Functions.tla file in TLAPS is not aligned with the Functions.tla version from the CommunityModules repository. Similarly, the TLAPS version of SequencesExt.tla has diverged from the SequencesExt.tla in CommunityModules. This discrepancy causes issues in VSCode when the LSP proof extension is enabled, as TLAPS overrides the CommunityModules versions, preventing TLC from accessing the latest definitions.

TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef)
Running breadth-first search Model-Checking with fp 61 and seed -8162497252886980334 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 46948] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla
Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/TLC.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /Users/markus/.opam/5.1.0/lib/tlapm/stdlib/SequencesExt.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/FiniteSetsExt.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/Integers.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/Sequences.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/Naturals.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /Users/markus/.opam/5.1.0/lib/tlapm/stdlib/FiniteSets.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/Relation.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/CommunityModules-deps.jar!/Relation.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-8661331616785400850/Folds.tla (jar:file:/Users/markus/.vscode/extensions/tlaplus.vscode-ide-2024.10.192237/tools/CommunityModules-deps.jar!/Folds.tla)
Parsing file /Users/markus/.opam/5.1.0/lib/tlapm/stdlib/Functions.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Functions
Semantic processing of module SequencesExt
Semantic processing of module Folds
Semantic processing of module FiniteSetsExt
Semantic processing of module Relation
Semantic processing of module abs
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module MCabs
Semantic errors:
*** Errors: 1
line 38, col 34 to line 38, col 52 of module MCabs
Unknown operator: `LongestCommonPrefix'.
SANY finished.
Starting... (2024-10-28 11:17:23)
Parsing or semantic analysis failed.
Finished in 299ms at (2024-10-28 11:17:23)

Could TLAPS consume the modules from the CommunityModules? Related: #27

@lemmy lemmy added the bug An error, usually in the code. label Oct 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug An error, usually in the code.
Development

No branches or pull requests

1 participant