Add Coq and agda cubes

core/cubes/agda.el

@@ -0,0 +1,42 @@
+;;; Agdacube --- Agda support for FG42 -*- lexical-binding: t; -*-
+;;
+;; Copyright (c) 2010-2023 Sameer Rahmani & Contributors
+;;
+;; Author: Sameer Rahmani <lxsameer@gnu.org>
+;; URL: https://ziglab.com/FG42/FG42
+;; Version: 3.0.0
+;;
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+;;
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+;;
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+;;
+;;; Commentary:
+;;; Code:
+(require 'fg42/cube)
+(require 'fg42/utils)
+
+
+(defcube fg42/agda-cube
+  "Integrate Agda-mode with Fg42"
+  (:title "Agda cube"
+          :flag-default t
+          :flag agda)
+  (load-file
+   (let* ((coding-system-for-read 'utf-8)
+          (home (getenv "HOME"))
+          (cabal-bin (concat home "/.cabal/bin/")))
+     (add-to-list 'exec-path cabal-bin)
+     (shell-command-to-string (concat cabal-bin "agda-mode locate")))))
+
+
+(provide 'cubes/agda)
+;;; agda.el ends here

core/cubes/proof.el

@@ -0,0 +1,41 @@
+;;; ProofGeneralCube --- ProofGeneral support for FG42 -*- lexical-binding: t; -*-
+;;
+;; Copyright (c) 2010-2023 Sameer Rahmani & Contributors
+;;
+;; Author: Sameer Rahmani <lxsameer@gnu.org>
+;; URL: https://ziglab.com/FG42/FG42
+;; Version: 3.0.0
+;;
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+;;
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+;;
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+;;
+;;; Commentary:
+;;; Code:
+(require 'fpkg)
+(require 'fg42/cube)
+(require 'fg42/utils)
+
+
+(defcube fg42/proof-general-cube
+  "Integrate Proof General with Fg42"
+  (:title "Proof General cube"
+          :flag-default t
+          :flag proof-general)
+
+  (fpkg/use proof-general)
+  (fpkg/use company-coq
+    :config (add-hook 'coq-mode-hook #'company-coq-mode)))
+
+
+(provide 'cubes/proof)
+;;; proof.el ends here