rocq-build-troubleshoot

Fast workflow to diagnose and fix Rocq/Coq compile errors in this repository, especially missing imports after links/simulate splits and per-file compile checks.

1. Uruchom skill, gdy plik .v nie kompiluje się prawidłowo i potrzebujesz szybkiej, ukierunkowanej naprawy. Skill pracuje w kontekście projektu RocqOfRust z flagami -R . RocqOfRust -impredicative-set.

2. Zacznij od reprodukcji błędu, uruchamiając kompilator na konkretnym pliku: coqc -R . RocqOfRust -impredicative-set ścieżka/do/pliku.v. Skill przeanalizuje komunikat błędu i zaproponuje konkretne kroki naprawy.

3. Jeśli błąd dotyczy brakującego modułu lub ścieżki ładowania, dodaj jawną deklarację Require Import w pliku, który się nie kompiluje. Unikaj polegania na usuniętych modułach agregujących; preferuj importy per-funkcja w katalogach links i simulate.

4. Gdy błąd wskazuje na niezgodność kolejności argumentów lub typu w wywołaniu run_*, porównaj lokalną sygnaturę funkcji run_* w pliku links/ i wyrównaj kolejność argumentów dokładnie. Usuń symbole zastępcze _, chyba że są wymagane przez parametry niejawne.

5. Jeśli literały Range nie przechodzą wnioskowania typu, użyj notacji rekordowej z jawnie typowanymi zerami: {| Range.start := (0 : usize); Range.end_ := (0 : usize) |}.

6. Po wprowadzeniu zmian ponownie skompiluj dotknięty plik poleceniem coqc z tymi samymi flagami. Opcjonalnie uruchom make ścieżka/do/pliku.vo, aby sprawdzić zależności. Pamiętaj, aby utrzymywać naprawy minimalne i lokalne, nie przywracając usuniętych agregatorów.