From 56d16ad1bad75d919216a4d09233e0da1a7c00b1 Mon Sep 17 00:00:00 2001
From: Sameer Rahmani <lxsameer@gnu.org>
Date: Wed, 31 May 2023 18:17:05 +0100
Subject: [PATCH] Add Coq and agda cubes

---
 core/cubes/agda.el  | 42 ++++++++++++++++++++++++++++++++++++++++++
 core/cubes/proof.el | 41 +++++++++++++++++++++++++++++++++++++++++
 core/fg42/proof.el  |  0
 3 files changed, 83 insertions(+)
 create mode 100644 core/cubes/agda.el
 create mode 100644 core/cubes/proof.el
 create mode 100644 core/fg42/proof.el

diff --git a/core/cubes/agda.el b/core/cubes/agda.el
new file mode 100644
index 0000000..aa3e21d
--- /dev/null
+++ b/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
diff --git a/core/cubes/proof.el b/core/cubes/proof.el
new file mode 100644
index 0000000..641c1cc
--- /dev/null
+++ b/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
diff --git a/core/fg42/proof.el b/core/fg42/proof.el
new file mode 100644
index 0000000..e69de29