軟件基礎 - 自動分級

爲了學習Coq，我下載了本傑明皮爾斯的電子書軟件基金會從here，並提取內容。我現在開始通過Basics.v的練習，直接在Vim中編輯文件。軟件基礎 - 自動分級

我想自動評分我的答案（例如跟蹤我的分數和時間）。

爲此，我按照Makefile中給出的順序針對每個.v文件運行coqc。因此，我是now able to invoke，例如， coqtop -batch -l BasicsTest.v。

但是，雖然這會報告該章節的可用分數，但它不會報告我的分數。（我是中途通過章節，並深信我的答案至今是正確的，因爲coqtop -batch -l Basics.v無誤的執行。）

我懷疑我忽略撥打或勒柯克的調用將產生一個分的成績對我迄今爲止的答案。如果是這樣，那是什麼？

2017-08-01 sampablokuper

幾乎每個人都使用交互式編輯器來解決Coq問題，而不是文本編輯器以及批處理模式。你可能想看看coqide/proofgeneral。它會讓你的生活更輕鬆。 – gallais

@gallais，感謝您的幫助:)我對CoqIDE的回憶是，它缺少一個好的文本編輯界面。前一段時間，我和證明將軍一起呆了一段時間，可能會回到它。我喜歡它試圖達到的目標，但與使用文本編輯器和Bash相比，它仍然感到麻煩。我的主觀印象是，它讓Emacs變得更慢，更容易崩潰：（ – sampablokuper

BasicsTest.v在當前版本的軟件基金會中未生成等級。你可以通過它來看看它的作用：它只是通過練習，執行一些基本檢查並報告結果。但是，根據這些檢查的結果不會生成分數。

如果你的定義和證明是否齊全（例如，不Admitted）和勒柯克的typechecker接受他們，你可以有合理的信心，答案是正確的，除非東西在你的開發打破勒柯克的邏輯（一致性在這個不太可能早期階段），或者你偶然發現了一個bug（極不可能）。

來源

2017-08-01 17:34:42

autograder當前不完整。我們希望在接下來的幾個月內完成它，並在我們這樣做時使它可用。但是，正如Rob所說，它實際上並沒有告訴你，通過在當前的測試版本中運行BasicsTest.v所獲得的結果。

來源

2017-08-02 13:14:39

假設這是真正的本傑明皮爾斯，感謝你創造這種鼓舞人心的教育材料，並使它們可用於部門之外的人，這意味着很多！期待完成的autograder。一旦發佈，請隨時更新此答案。再次感謝:) – sampablokuper

軟件基礎 - 自動分級

回答

相關問題