Bu, Ubuntu Online, Fedora Online, Windows çevrimiçi emülatörü veya MAC OS çevrimiçi emülatörü gibi birden fazla ücretsiz çevrimiçi iş istasyonumuzdan birini kullanarak OnWorks ücretsiz barındırma sağlayıcısında çalıştırılabilen coqchk.opt komutudur.
Program:
ADI
coqchk - Coq Proof Checker derlenmiş kitaplıklar doğrulayıcı
SİNOPSİS
koklamak [ seçenekleri ] modüller
TANIM
koklamak için derlenmiş kitaplıkların (coqc tarafından üretilen .vo dosyaları) bağımsız denetleyicisidir.
Coq Kanıtı Asistanı. Daha fazla bilgi için Başvuru Kılavuzuna bakın. ile döner
istenen tüm görevler başarılı olursa 0 kodundan çıkın. Sıfır olmayan bir dönüş kodu şu anlama gelir:
bir şeyler ters gitti: bazı kitaplıklar bulunamadı, bozuk içerik, tür denetimi
başarısızlık vb.
modüller kontrol edilecek modüllerin bir listesidir. Modüller kısa veya
nitelikli isim.
SEÇENEKLER
-I dir --Dahil etmek dir
dizin ekle dir dahil etme yolunda
-R dir kokdir
fiziksel haritayı özyinelemeli olarak dir mantıklı kokdir
-sessiz
coqchk'u daha az ayrıntılı yapar.
-Kabul et modül
belirtilen modülü ve tüm bağımlılıklarını güvenilir olarak etiketleyin ve
diğer seçenekler tarafından açıkça talep edilmediği sürece yeniden kontrol edilir.
-norek modül
verilen modülün kontrol edilmeden doğrulanacağını belirtir.
bağımlılıklar.
-M, --hafıza
denetleyici tarafından kullanılan belleğin bir özetini görüntüler.
-Ö, --çıktı-bağlam
doğrulanmış mantıksal içeriğin bir özetini görüntüler: varsayımlar ve
öngörülebilirlik kullanımı.
-öngörülü-küme
denetleyicinin bu bayrakla derlenmiş kitaplıkları kabul etmesine izin verir.
-v coqchk sürümünü yazdırın ve çıkın.
-coqlib dir
standart kitaplığın varsayılan konumunu geçersiz kılar.
-nerede coqchk standart kitaplık konumunu yazdırın ve çıkın.
-H, --yardım et
seçeneklerin listesini yazdır
onworks.net hizmetlerini kullanarak coqchk.opt'u çevrimiçi kullanın
