Hacktoberfest 2026: as issues que os mantenedores marcaram para outubro, abertas e boas para iniciantes. Ver issues do Hacktoberfest

statechart: a relative TLA2TOOLS or JAVA path fails, because TLC runs in the snapshot folder

Aberta Para iniciantes
#973 0 comentários 0 reações 0 responsáveis Ver no GitHub

Mantenedores costumam responder em até 1 dia

Ninguém assumiu esta issue ainda.

Avaliação

Dificuldade
2/5
Tempo estimado
1-3 horas
Facilidade para iniciantes
78/100
Tipo de issue
Bug
Clareza
Claramente especificada
Status de atividade
Ativa
Stack de tecnologia
node.js, typescript
Domínio
tooling

Direção de pesquisa

Leia pstack/skills/statechart/scripts/tlc-tools.mjs e pstack/skills/statechart/scripts/statechart.mjs, com foco em como findTlc resolve TLA2TOOLS e JAVA e em como tlc() define seu diretório de trabalho. Reproduza o problema com os caminhos relativos e absolutos da issue. O trabalho estará concluído quando os caminhos aceitos a partir do diretório do chamador também funcionarem a partir da pasta do snapshot e from-spec puder executar o TLC.

Escrita pelo modelo de indexação a partir do texto da issue.

Descrição

What happens

findTlc in pstack/skills/statechart/scripts/tlc-tools.mjs checks that TLA2TOOLS and JAVA exist from the caller's working directory, then returns them as given. tlc() in statechart.mjs starts java with cwd set to the folder of the spec's snapshot copy under $TMPDIR/statechart-inputs-*/. Java resolves a relative -cp against that folder, so it cannot find the jar, and from-spec exits with cannot run TLC. A relative JAVA with a slash, such as ./jdk/bin/java, starts from the same folder.

Reproduce

Tested at 9e88dad on macOS with Node 25.8.0. The stand-in java prints the folder it runs in and whether it can see the -cp jar.

mkdir repro && cd repro && mkdir tools && touch tools/tla2tools.jar
cat > fake-java <<'EOF'
#!/bin/sh
cp=""; prev=""; for a in "$@"; do [ "$prev" = "-cp" ] && cp="$a"; prev="$a"; done
echo "java runs in: $PWD" >&2
if [ -e "$cp" ]; then echo "jar $cp: found" >&2; else echo "jar $cp: not found" >&2; fi
exit 1
EOF
chmod +x fake-java
printf -- '---- MODULE Spec ----\nEXTENDS Naturals\nVARIABLE x\nInit == x = 0\nNext == x'"'"' = x\n====\n' > Spec.tla
printf 'INIT Init\nNEXT Next\n' > Spec.cfg
S=/path/to/pstack/skills/statechart/scripts/statechart.mjs
export JAVA=$PWD/fake-java
TLA2TOOLS=tools/tla2tools.jar node $S from-spec Spec.tla   # writes Spec.map.mjs
TLA2TOOLS=tools/tla2tools.jar node $S from-spec Spec.tla
TLA2TOOLS=$PWD/tools/tla2tools.jar node $S from-spec Spec.tla

With the relative path:

cannot run TLC with .../fake-java -cp tools/tla2tools.jar: java exited 1:
  java runs in: $TMPDIR/statechart-inputs-B8EIpr/<absolute path of repro>
  jar tools/tla2tools.jar: not found

With the absolute path, java runs in the same snapshot folder and prints jar <absolute path>: found.

Expected

A TLA2TOOLS or JAVA path that exists from the caller's directory, which findTlc already checks, also works when TLC runs.

Linguagem predominante
TypeScript
Estrelas
13.9k
Forks
1.4k
Merge médio
7h 5min
PRs com merge (30d)
150

Preparar o ambiente

Este projeto não oferece contêiner de desenvolvimento, Dockerfile nem guia de contribuição, então a configuração fica por sua conta: comece pelo README e veja nosso guia da primeira contribuição para os passos gerais.

Primeiros passos

  1. Leia a issue inteira e depois o guia de contribuição do projeto.
  2. Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
  3. Faça um fork do repositório e trabalhe em uma branch.
  4. Abra um pull request que referencie o número da issue.

Mais de cursor/plugins

Todas as issues de cursor/plugins

Issues semelhantes

Mais issues de TypeScript

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.