diff options
| author | Emilio Jesus Gallego Arias | 2018-12-17 11:55:51 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-17 11:55:51 +0100 |
| commit | 854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (patch) | |
| tree | 107a22e58dcf0fb492a30561b340c9f033de3990 /test-suite | |
| parent | 6095ef4d0aac719776dcc949591d1413cf2a5354 (diff) | |
| parent | a9e87e0b25cf11192d11da4499c3c3122f11a0c4 (diff) | |
Merge PR #9206: [stm] join the tip of the document even when fixing a proof (fix #9204)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | test-suite/ide/join-sync.fake | 20 | ||||
| -rw-r--r-- | test-suite/ide/join.fake | 20 |
3 files changed, 41 insertions, 1 deletions
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 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 |