From fa223ceafdbc94768884d35af2f464deafd2e445 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Tue, 14 Aug 2018 23:21:55 +0200 Subject: [PATCH 1/7] Added basic coq support --- modules/lang/coq/config.el | 9 +++++++++ modules/lang/coq/packages.el | 4 ++++ 2 files changed, 13 insertions(+) create mode 100644 modules/lang/coq/config.el create mode 100644 modules/lang/coq/packages.el diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el new file mode 100644 index 000000000..926c69592 --- /dev/null +++ b/modules/lang/coq/config.el @@ -0,0 +1,9 @@ +;;; lang/coq/config.el -*- lexical-binding: t; -*- + +(defvar +coq-pg-loc "/home/patrl/GitHub/PG/generic") + +(def-package! proof-site + :load-path +coq-pg-loc + :defer t + :mode ("\\.v\\'" . coq-mode) + :hook (coq-mode . company-coq-mode)) diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el new file mode 100644 index 000000000..d813083d3 --- /dev/null +++ b/modules/lang/coq/packages.el @@ -0,0 +1,4 @@ +;; -*- no-byte-compile: t; -*- +;;; lang/coq/packages.el + +(package! company-coq) From 4280ea3418755cf981f93f0736390349a45c2783 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Tue, 14 Aug 2018 23:30:20 +0200 Subject: [PATCH 2/7] Added readme. --- modules/lang/coq/README.org | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 modules/lang/coq/README.org diff --git a/modules/lang/coq/README.org b/modules/lang/coq/README.org new file mode 100644 index 000000000..1a59ea85a --- /dev/null +++ b/modules/lang/coq/README.org @@ -0,0 +1,13 @@ +#+TITLE: :lang coq + +This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]], with code completion via [[https://github.com/cpitclaudel/company-coq][company-coq]]. + +* Install +Unfortunately, Proof General needs to be installed manually. + +#+BEGIN_SRC sh +git clone https://github.com/ProofGeneral/PG $PG-LOC && cd $PG-LOC +make +#+END_SRC + +Manually set the variable ~+coq-pg-loc~ to the value of $PG-LOC in your doom config. From 2929b58cdef7b6fe0e1ee2c6e066b926dc4891a1 Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Wed, 15 Aug 2018 08:17:20 +0200 Subject: [PATCH 3/7] Modified variable --- modules/lang/coq/config.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 926c69592..a8a600663 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,6 +1,7 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- -(defvar +coq-pg-loc "/home/patrl/GitHub/PG/generic") +;; set this to the absolute path of the folder containing proof-site.el, e.g. /home/$USER/GitHub/PG/generic +(defvar +coq-pg-loc nil) (def-package! proof-site :load-path +coq-pg-loc From f5c1be44baac162ecaa1f40fc5427a3da4f8e14d Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Wed, 15 Aug 2018 08:33:38 +0200 Subject: [PATCH 4/7] Added quelpa recipe --- modules/lang/coq/config.el | 3 --- modules/lang/coq/packages.el | 2 ++ 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index a8a600663..62bbe97fe 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,8 +1,5 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- -;; set this to the absolute path of the folder containing proof-site.el, e.g. /home/$USER/GitHub/PG/generic -(defvar +coq-pg-loc nil) - (def-package! proof-site :load-path +coq-pg-loc :defer t diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el index d813083d3..3ae652118 100644 --- a/modules/lang/coq/packages.el +++ b/modules/lang/coq/packages.el @@ -1,4 +1,6 @@ ;; -*- no-byte-compile: t; -*- ;;; lang/coq/packages.el +(package! proof-general :recipe (:fetcher github :repo "ProofGeneral/PG" :files ("*"))) + (package! company-coq) From 55b5c7711b83d32c01b4be3c3e67d0bc3184fbab Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Wed, 15 Aug 2018 08:34:21 +0200 Subject: [PATCH 5/7] Updated readme --- modules/lang/coq/README.org | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/modules/lang/coq/README.org b/modules/lang/coq/README.org index 1a59ea85a..680555966 100644 --- a/modules/lang/coq/README.org +++ b/modules/lang/coq/README.org @@ -1,13 +1,3 @@ #+TITLE: :lang coq This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]], with code completion via [[https://github.com/cpitclaudel/company-coq][company-coq]]. - -* Install -Unfortunately, Proof General needs to be installed manually. - -#+BEGIN_SRC sh -git clone https://github.com/ProofGeneral/PG $PG-LOC && cd $PG-LOC -make -#+END_SRC - -Manually set the variable ~+coq-pg-loc~ to the value of $PG-LOC in your doom config. From 6393ebe16bef4e581726329f7adc41022b0cd96f Mon Sep 17 00:00:00 2001 From: Patrick Elliott Date: Sat, 18 Aug 2018 14:51:21 +0200 Subject: [PATCH 6/7] Removed redundant config --- modules/lang/coq/config.el | 2 -- 1 file changed, 2 deletions(-) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 62bbe97fe..ea8974723 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -1,7 +1,5 @@ ;;; lang/coq/config.el -*- lexical-binding: t; -*- (def-package! proof-site - :load-path +coq-pg-loc - :defer t :mode ("\\.v\\'" . coq-mode) :hook (coq-mode . company-coq-mode)) From 48c531e76cadd3576e303e33856ca0b87fdefd2d Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Sat, 18 Aug 2018 23:45:36 +0200 Subject: [PATCH 7/7] lang/coq: move config.el to autoload.el The auto-mode-alist entry for coq-mode and friends are already added by proof-general's autoloads file, and neither coq-mode nor company-coq-mode belong to proof-site specifically, so they shouldn't be treated like they are (this could cause autoloading errors). The `def-package!` block altogether is unnecessary. The only thing we need is to enable `company-coq-mode` on coq-mode-hook. However, having a one-line config.el is a tad excessive, so we put it in autoload.el instead. --- modules/lang/coq/autoload.el | 4 ++++ modules/lang/coq/config.el | 5 ----- 2 files changed, 4 insertions(+), 5 deletions(-) create mode 100644 modules/lang/coq/autoload.el delete mode 100644 modules/lang/coq/config.el diff --git a/modules/lang/coq/autoload.el b/modules/lang/coq/autoload.el new file mode 100644 index 000000000..624185018 --- /dev/null +++ b/modules/lang/coq/autoload.el @@ -0,0 +1,4 @@ +;;; lang/coq/autoload.el -*- lexical-binding: t; -*- + +;;;###autoload +(add-hook 'coq-mode-hook #'company-coq-mode) diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el deleted file mode 100644 index ea8974723..000000000 --- a/modules/lang/coq/config.el +++ /dev/null @@ -1,5 +0,0 @@ -;;; lang/coq/config.el -*- lexical-binding: t; -*- - -(def-package! proof-site - :mode ("\\.v\\'" . coq-mode) - :hook (coq-mode . company-coq-mode))