From 00263f3211c67b16a488c6b0c2bc6432a1837256 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 13 Dec 2018 10:23:23 +0100
Subject: [test] for #9204

---
 test-suite/ide/join.fake | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/ide/join.fake

(limited to 'test-suite')

diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake
new file mode 100644
index 0000000000..c4c696ad9a
--- /dev/null
+++ b/test-suite/ide/join.fake
@@ -0,0 +1,20 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Error resiliency
+#
+
+ADD { Section x. }
+ADD { Lemma x : True. }
+ADD { Proof using. }
+ADD here { trivial. }
+ADD { fail. }
+ADD { Qed. }
+ADD { Lemma y : True. }
+ADD { Proof using. }
+ADD { trivial. }
+ADD { Qed. }
+ADD { End x. }
+FAILJOIN
+ASSERT TIP here
+ABORT
-- 
cgit v1.2.3


From a9e87e0b25cf11192d11da4499c3c3122f11a0c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 13 Dec 2018 10:56:13 +0100
Subject: [test] for join when error resiliency on and async-proofs off

---
 test-suite/Makefile           |  2 +-
 test-suite/ide/join-sync.fake | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/ide/join-sync.fake

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 9d2277c37e..530671e1a1 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -569,7 +569,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
+	  $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake
new file mode 100644
index 0000000000..236028ce46
--- /dev/null
+++ b/test-suite/ide/join-sync.fake
@@ -0,0 +1,20 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Error resiliency + async proofs off
+# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on")
+#
+
+ADD { Lemma x : True. }
+ADD { Proof using. }
+ADD here { trivial. }
+ADD { fail. }
+ADD { Qed. }
+ADD { Lemma y : True. }
+ADD { Proof using. }
+ADD { trivial. }
+ADD { Qed. }
+WAIT
+FAILJOIN
+ASSERT TIP here
+ABORT
-- 
cgit v1.2.3