Beweren en bewijzen/de opzet/gereedschap/Coq/technische problemen

Hier verzamelen we problemen waar men tegen aanloopt in het gebruik van de Coq web interface. Wanneer je een probleem hebt of juist hebt opgelost, maak daar dan melding van op deze pagina. Neem deze pagina op in je volglijst om op de hoogte te blijven.

Probleem	Omschrijving	Oplossing
Copy/Paste werkt niet	Copy/Paste vanaf de Werkplaats naar de Coq webinterface werkt bij sommige browsers niet, omdat er onzichtbare symbolen tussen de tekst worden gestopt die Coq niet snapt.	Een oplossing kan zijn om eerst naar een reguliere tekstverwerker te kopieeren.
bewijsregels falen	Om onduidelijke redenen kunnen bewijsregels soms niet toegepast worden. imp_i A1 werkt bijvoorbeeld nooit. N.b. werkt nu wel maar misschien zijn er andere namen die het niet doen.	Kies andere namen voor de aannames. Probeer het bij voorkeur eens met een hele rare lange naam die Coq zeker niet intern zal gebruiken. imp_i H1 werkt wel. N.b. de ergste problemen zijn verholpen maar er kunnen nog namen zijn die je niet mag gebruiken.
Wilde refreshes	Als Coq een stap niet heeft kunnen voltooien begint hij soms de refreshen als een gek, zonder zichtbaar effect. Heb de precieze voorwaarden nog niet kunnen vinden (FF2.0.0.14). Dit refresh probleem heb ik (Dirk van der Linden 2 jun 2008 13:24 (CEST)) ook geconstateerd als Coq een lange tijd openstaat (>1 uur) en ik daarna weer iets wil gaan doen. Zodra ik een stap omhoog of omlaag gaat gaat het allemaal oneindig refreshen en moet ik het hele venster afsluiten.
(exi x, Q x) <> (exists x, Q x)	Op één of andere manier zijn exi en exists (en all en forall) niet hetzelfde. De ene keer werkt de afkorting beter dan het hele woord en de andere keer is het net andersom. // All exi veranderen naar exists is bij de oefenen opgaven niet echt een oplossing want ze beteken blijkbaar echt iets heel anders.	Jasper Berendsen: Gebruik alleen exist en forall. Dat moet gewoon goed werken en staat ook overal als het goed is.
display met Focus	Als in het bewijs het commando Focus wordt gebruikt kan de weergave van de bewijsboom verdwijnen	Helaas nog geen oplossing. Focus is handig tijdens het bewijzen maar verwijder het uiteindelijk.
Weergave niet in sync met stappen. Ook te karakteriseren als: undo werkt op een gegeven moment niet meer.	Als je de afbeelding bekijkt zie je wat ik bedoel. Stap H15 is nog niet uitgevoerd, maar in de weergave lijkt het alsof dit al wel is gebeurd. Ik heb deze stap eerder ook wel uitgevoerd maar heb een stappen terug gedaan om wat te wijzigen. Dit probleem heb ik ook bij mijn bewijs gehad, het komt constant voor zodra het Coq script wat groter begint te worden en je enkele stappen omhoog en omlaag gaat. Ik heb er geen oplossing voor kunnen vinden behalve je script compleet opnieuw erin pasten en het weer helemaal laten evalueren. Maar op die manier dwingt Coq je wel bijna om maar gewoon blind te werken en Coq pas te gebruiken als je denkt dat je enkele stappen goed gedaan hebt. (Dirk van der Linden 6 jul 2008 09:31 (CEST))	Cezary: Het probleem is dat Coq een (zeer) eindige stack gebruikt voor de undo's. Door voor je bewijs het commando: Set Undo 100. te geven, maak je die stack groter. Jasper Berendsen: Een andere oplossing is natuurlijk het bewijs in kleine bewijsjes opsplitsen met hulptheorema's.
Bewijsboom wordt niet gegenereerd	Ik kan voor het bewijs bij mijn werkstuk geen bewijsboom genereren. Ik vermoed dat dit ook met de grote van het bewijs heeft te maken aangezien ik geen Focus gebruik of gebruikt heb. (Onno Berfelo 7 jul 2008 11:05 (CEST))	Voor grote bewijzen moet je wel geduld hebben. Het genereren van de bewijsboom kost Coq dan de nodige tijd. Gebruik Hypothesis voor je onderdelen, zie Coq pagina. Je kunt hulp theorema's gebruiken. Zie Beweren_en_bewijzen/de_opzet/gereedschap/Coq#Grote_bewijzen.