콕 증명 도우미 이맥스 환경의 시작
2024-07-05 Note coq emacs ide notes proofassistants교수님의 프로젝트의 일부이다.
Coq는 주로 소프트웨어와 수학적 증명의 형식적 검증에 사용되는 증명 도우미이다. 수학적 주장, 정의, 정리를 표현하기 위한 공식 언어와 이러한 주장에 대한 증명을 대화식으로 구성하고 검증하는 메커니즘을 제공한다.
콕 설치는 오펨 활용하라 - 스코드 여기서 시작!
CANCELLED coqtop 이 필요하다고 한다.
일단 우분투에서 필요한 구성 요소를 설치한다. 둠 메뉴얼을 보니 coqtop 을 설치하란다.
Make sure you have Coq installed and that the coqtop command is available. This comes with a standard installation of Coq. You can use your linux distribution’s Coq package or one of the methods given on the Coq website.
# ➜ coqtop
# 명령어 'coqtop' 을(를) 찾을 수 없습니다. 그러나 다음을 통해 설치할 수 있습니다:
# sudo snap install coq-prover # version 2023-11-0, or
# sudo snap remove coq-prover
# sudo apt install coq # version 8.16.1+dfsg-1build2
# 'snap info coq-prover'에서 추가적인 버전을 확인하십시오.
# sudo apt install coq # version 8.16.1+dfsg-1build2
# sudo apt install opam
# sudo apt-get remove coq opam이렇게 하면 된다. 안전하다 우분투 패키지가. 1기가 바이트 정도 설치한다
스냅으로 설치해야겠다. 최신 안정 버전 말이다. 이 버전은 vscoq과 lsp 로도 연동할 것이다.
This snap contains the Coq prover version 8.18.0 along with CoqIDE and number of Coq plugins and libraries. Please refer to
https://github.com/coq/platform/blob/main/doc/README%7E8.18%7E2023.11.md
보자. 버전을 확인하고. coqide 도 있다.
➜ coqtop --version
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.1
(base) ~ via v20.14.0둠이맥스에서는 이맥스의 멋진 패키지를 활용한다.
A generic Emacs interface for proof assistants. (team n.d.) “Proof General - A generic Emacs interface for proof assistants.”
그리고 doomemacs/snippets/tree/master/coq-mode - github.com 둠이맥스의 스니펫들을 제공한다. 그러면 준비는 다 된 것이다. 기본으로 충분하다.
이것이 이맥스에서 할 수 있는 기본적인 설정이다. 이제 할 일은 직접 해보는 것이다. 정주희 (2024) Coq 스터디 가이드 여기에 실제 교재와 더불어 학습 내용을 기록 하면 된다.
둠이맥스 환경 설정의 예
;; init.el
;; (:unless IS-TERMUX (coq)) ; proofs-as-programs
;; /hrs-dotfiles/emacs/.config/emacs/configuration.org
;; I like to disable =abbrev-mode=; it has a ton of abbreviations for Coq, but they've always been unpleasant surprises for me.
;; Similarly, =flycheck-mode= seems to do more harm than good.
;; The Proof General splash screen's pretty cute, but I don't need to see it every time.
;; The default Proof General layout stacks the code, goal, and response buffers on top of each other. I like to keep my code on one side and my goal and response buffers on the other.
;; Have point follow the end of the locked region when asserting and undoing proof commands, but don't lock it to the end.
;; Proof General usually evaluates each comment individually. In literate programs, this can result in evaluating a /ton/ of comments. This evaluates a series of consecutive comments as a single comment.
;; I bind the up and down arrow keys in Coq to evaluating and retracting the next and previous statements. This is more convenient for me than the default bindings of =C-c C-n= and =C-c C-u=.
(when (modulep! :lang coq)
(use-package! company-coq
:commands company-coq-mode
:bind (:map company-coq-map
;; ("<tab>" . company-complete)
("M-<return>"))
:bind (:map coq-mode-map
("C-M-h" . company-coq-toggle-definition-overlay))
;; :custom
;; (company-coq-disabled-features
;; '(hello prettify-symbols smart-subscripts dynamic-symbols-backend))
;; (company-coq-prettify-symbols-alist
;; '(("|-" . 8866)
;; ("True" . 8868)
;; ("False" . 8869)
;; ("->" . 8594)
;; ("-->" . 10230)
;; ("<-" . 8592)
;; ("<--" . 10229)
;; ("<->" . 8596)
;; ("<-->" . 10231)
;; ("==>" . 10233)
;; ("<==" . 10232)
;; ("++>" . 10239)
;; ("<++" . 11059)
;; ("fun" . 955)
;; ("forall" . 8704)
;; ("exists" . 8707)
;; ("/\\" . 8743)
;; ("\\/" . 8744)
;; ("~" . 172)
;; ("+-" . 177)
;; ("<=" . 8804)
;; (">=" . 8805)
;; ("<>" . 8800)
;; ("*" . 215)
;; ("++" . 10746)
;; ("nat" . 120029)
;; ("Z" . 8484)
;; ("N" . 8469)
;; ("Q" . 8474)
;; ("Real" . 8477)
;; ("bool" . 120121)
;; ("Prop" . 120031)))
;; :custom-face
;; (company-coq-features/code-folding-bullet-face ((t (:weight bold))))
:functions (cape-company-to-capf)
:config
(setq coq-prog-name "/home/junghan/.opam/default/bin/coqtop")
(add-hook 'company-coq-mode-hook
#'(lambda ()
;; (company-mode -1)
(require 'cape)
(setq-local completion-at-point-functions
(mapcar #'cape-company-to-capf
company-coq-enabled-backends))))
(add-hook 'coq-mode-hook #'(lambda ()
(abbrev-mode 0)
(flycheck-mode 0)))
(evil-define-key 'normal coq-mode-map (kbd "C-<down>") 'proof-assert-next-command-interactive) ; coq-ide style
(evil-define-key 'insert coq-mode-map (kbd "C-<down>") 'proof-assert-next-command-interactive)
(evil-define-key 'normal coq-mode-map (kbd "C-<up>") 'proof-undo-last-successful-command)
(evil-define-key 'insert coq-mode-map (kbd "C-<up>") 'proof-undo-last-successful-command)
)
(use-package! coq-lookup
:ensure nil
:bind ("C-h q" . coq-lookup)
:custom
(coq-lookup-browse-pdf-function
'(lambda (pdf page) (call-process "open" nil nil nil pdf)))
;; (coq-lookup-pdf "~/.local/share/coq/coq-8.15.2-reference-manual.pdf")
(coq-lookup-pdf "~/sync/markdown/pdf/coq-8.18.0-reference-manual.pdf"))
;; (use-package! prover
;; :after coq)
)