Merge branch 'tchajed/add-tests' into 'master'

Add tests and test infrastructure

See merge request !4

.gitignore

@@ -5,5 +5,6 @@
 .*.aux
 
 .Makefile.coq.d
+.coqdeps.d
 Makefile.coq
 Makefile.coq.conf

Makefile.coq.local

+# Run tests interleaved with main build.  They have to be in the same target for this.
+real-all: $(if $(NO_TEST),,test)
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
+COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
+	    REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
+	  else \
+	    REF="tests/$$TEST.ref"; \
+	  fi && \
+	  echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
+	  TMPFILE="$$(mktemp)" && \
+	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
+	  $(if $(COQ_OLD),true, \
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
+	  ) && \
+	  rm -f "$$TMPFILE" && \
+	  touch $@

tests/string_ident.ref

+"test_invalid_ident"
+     : string
+The command has indeed failed with message:
+Uncaught Ltac2 exception: InvalidIdent ("has a space")
+"test_not_string"
+     : string
+The command has indeed failed with message:
+Uncaught Ltac2 exception: NotStringLiteral (constr:(4))
+"test_not_literal"
+     : string
+The command has indeed failed with message:
+Uncaught Ltac2 exception: NotStringLiteral (constr:(s))

tests/string_ident.v

+From iris_string_ident Require Import ltac2_string_ident.
+From Coq Require Import Strings.String.
+Open Scope string.
+
+Lemma test_basic_ident : forall (n:nat), n = n.
+Proof.
+  let x := string_to_ident "n" in
+  intros x.
+  exact (eq_refl n).
+Qed.
+
+Lemma test_in_scope (n:nat) : n = n.
+Proof.
+  let x := string_to_ident "n" in exact (eq_refl n).
+Qed.
+
+Check "test_invalid_ident".
+Lemma test_invalid_ident : True.
+Proof.
+  Fail let x := string_to_ident "has a space" in
+       idtac x.
+Abort.
+
+Check "test_not_string".
+Lemma test_not_string : True.
+Proof.
+  Fail let x := string_to_ident 4 in
+       idtac x.
+Abort.
+
+Check "test_not_literal".
+Lemma test_not_literal (s:string) : True.
+Proof.
+  Fail let x := string_to_ident s in
+       idtac x.
+Abort.

theories/ltac2_string_ident.v

@@ -7,7 +7,7 @@ From iris.proofmode Require Import ltac_tactics.
 Import List.ListNotations.
 Local Open Scope list.
 
-Ltac2 Type exn ::= [ InvalidIdent(string) ].
+Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
 
 Module StringToIdent.
 
@@ -39,6 +39,7 @@ Module StringToIdent.
     match! s with
     | EmptyString => 0
     | String _ ?s' => Int.add 1 (coq_string_length s')
+    | _ => Control.throw (NotStringLiteral(s))
     end.
 
   Ltac2 compute c :=