rocq-build-troubleshoot

Skill do efektywnego diagnozowania i naprawiania błędów kompilacji plików .v w projekcie RocqOfRust. Specjalizuje się w rozwiązywaniu problemów z brakującymi importami po podziałach links/simulate oraz w sprawdzaniu kompilacji poszczególnych plików. Oferuje konkretne strategie naprawy: dodawanie jawnych deklaracji Require Import, wyrównywanie sygnatury funkcji run_*, oraz poprawne typowanie literałów Range. Workflow skupia się na minimalnych, lokalnych zmianach bez przywracania usuniętych modułów agregujących.

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.