6
Coq. Ilgili Yazılım Temelleri kitabındaki alıştırmaları tamamlamak için CoqIDE kullanıyorum. Basics.v'yi başarılı bir şekilde derleyebilirim, sonuçta Basics.vo ve Basics.glob dizinimden sonuçlanır. Induction.v'yi çalıştırmaya çalıştığımda çalışır. Derlemeyi denediğimde, evenb ve negb_involutive gibi eksik eksik referanslardan şikayet ediyor. Basics.v içeriğini Induction.v içine kopyalarsam, derler, ama açıkçası bu gitmek için bir yol değildir.Geçerli ortamda "X" referansı bulunamadı
Derleme Basics.v: Zaten böyle şeyler yaptığı gibi
Bu söz Coq error: The reference evenb was not found in the current environment bir kopyası olmaması gerekir. Basics.vo'nun dizinde olup olmadığını kontrol edin. Şimdi Induction.v derleyin. Bu son adım başarısız.
Şimdi denedim (SF'nin yeni bir kopyasını indirdim ve CoqIDE içindeki menüden derledim) ve herhangi bir hata almadım. Yaptığın şeyi biraz daha açıklayabilir misin? Hangi Coq-sürümünüz var? 8.5pl2 var. – larsr
Basics.v ve Induction.v içindeki her şeyi çözdüm. Seninle aynı versiyona sahibim. Belki de "boş" sürümlerini derlemeyi denemeliyim. Ben geri rapor edeceğim. – RaptorDotCpp
@larsr Yeni kopyayı da indirdim. CoqIDE'ı açtım, Basics.v dosyasını açtım ve derledim. Bu başarılı oldu. İndüksiyon.v açtıktan sonra derlemeyi denediğimde, daha önce olduğu gibi aynı hatayı aldım. Bu yüzden yeni kopya bile sistemimde derlenmiyor. Mac OS X El Capitan kullanıyorum. – RaptorDotCpp