Import from SkySkimmer/coq@911455d

.github/workflows/docker-action.yml

@@ -0,0 +1,29 @@
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ltac2-compiler.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.gitignore

@@ -0,0 +1,13 @@
+Makefile.coq*
+
+/src/g_tac2compile.ml
+
+*.a
+*.aux
+*.cm*
+*.d
+*.glob
+*.o
+*.vo*
+.merlin
+META*

Makefile

@@ -0,0 +1,19 @@
+MAKE_OPTS:= --no-builtin-rules
+
+TEST_GOALS:=$(filter test%, $(MAKECMDGOALS))
+
+.PHONY: submake
+submake: Makefile.coq
+	$(MAKE) $(MAKE_OPTS) -f Makefile.coq $(filter-out test%, $(MAKECMDGOALS))
+	+$(if $(TEST_GOALS),$(MAKE) $(MAKE_OPTS) -C tests $(patsubst tests/%,%,$(filter-out test, $(TEST_GOALS))))
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f $< -o $@
+
+%:: submake ;
+
+# known sources
+
+Makefile: ;
+
+_CoqProject: ;

README.md

@@ -0,0 +1 @@
+A compiler for Ltac2

_CoqProject

@@ -0,0 +1,9 @@
+-generate-meta-for-package coq-ltac2-compiler
+-Q src Ltac2Compiler
+-I src
+
+src/Ltac2Compiler.v
+src/g_tac2compile.mlg
+src/tac2compile.ml
+src/tac2compile.mli
+src/ltac2_compiler.mlpack

coq-ltac2-compiler.opam

@@ -0,0 +1,23 @@
+opam-version: "2.0"
+maintainer: "gaetan.gilbert@skyskimmer.net"
+version: "dev"
+
+homepage: "https://github.com/SkySkimmer/coq-ltac2-compiler"
+dev-repo: "git+https://github.com/SkySkimmer/coq-ltac2-compiler.git"
+bug-reports: "https://github.com/SkySkimmer/coq-ltac2-compiler/issues"
+license: "LGPL-2.1-only"
+
+synopsis: "Plugin to compile Ltac2 tactics using OCaml"
+description: """
+Plugin to compile Ltac2 tactics using OCaml."""
+
+build: [make "-j%{jobs}%" "test"]
+install: [make "install"]
+depends: [
+  "ocaml" {>= "4.09.0"}
+  "coq" {= "dev"}
+]
+
+authors: [
+  "Gaëtan Gilbert"
+]

src/Ltac2Compiler.v

@@ -0,0 +1 @@
+Declare ML Module "coq-ltac2-compiler.plugin".

src/dune

@@ -0,0 +1,8 @@
+(library
+ (name ltac2_compiler)
+ (public_name coq.ltac2-compiler)
+ (synopsis "Ltac2 compiler using OCaml")
+ (libraries coq-core.plugins.ltac2)
+ (flags :standard -w -40))
+
+(coq.pp (modules g_tac2compile))

src/g_tac2compile.mlg

@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+DECLARE PLUGIN "coq-ltac2-compiler.plugin"
+
+{
+
+open Util
+open Names
+open Pcoq
+
+let recursive_att = Attributes.bool_attribute ~name:"recursive"
+}
+
+VERNAC COMMAND EXTEND Ltac2Compile CLASSIFIED AS SIDEFF
+| #[ recursive = recursive_att ] [ "Ltac2" "Compile" reference_list(n) ] ->
+  { Tac2entries.perform_compile ?recursive n }
+END

src/ltac2_compiler.mlpack

@@ -0,0 +1,2 @@
+Tac2compile
+G_tac2compile