updated tests for ci

EugeneLoy · Feb 5, 2020 · f77c756 · f77c756
1 parent 5f4d214
commit f77c756
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 15 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -5,14 +5,14 @@ dist: bionic
 language: generic
 
 env:
-  - COQ_PACKAGE=coq-8.6.1 PYTHON_VERSION=3
-  - COQ_PACKAGE=coq-8.7.2 PYTHON_VERSION=3
-  - COQ_PACKAGE=coq-8.8.2 PYTHON_VERSION=3
-  - COQ_PACKAGE=coq-8.9.1ide PYTHON_VERSION=3
-  - COQ_PACKAGE=coq-8.6.1 PYTHON_VERSION=2
-  - COQ_PACKAGE=coq-8.7.2 PYTHON_VERSION=2
-  - COQ_PACKAGE=coq-8.8.2 PYTHON_VERSION=2
-  - COQ_PACKAGE=coq-8.9.1ide PYTHON_VERSION=2
+  - COQ_PACKAGE=coq-8.6.1 PYTHON_VERSION=3 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.7.2 PYTHON_VERSION=3 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.8.2 PYTHON_VERSION=3 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.9.1ide PYTHON_VERSION=3 LEGACY_COQ_VERSION=0
+  - COQ_PACKAGE=coq-8.6.1 PYTHON_VERSION=2 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.7.2 PYTHON_VERSION=2 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.8.2 PYTHON_VERSION=2 LEGACY_COQ_VERSION=1
+  - COQ_PACKAGE=coq-8.9.1ide PYTHON_VERSION=2 LEGACY_COQ_VERSION=0
 
 install:
   - sudo add-apt-repository -y ppa:jgross-h/many-coq-versions

diff --git a/test/kernel_test.py b/test/kernel_test.py
@@ -1,5 +1,6 @@
 import unittest
 import jupyter_kernel_test
+import os
 
 class KernelTests(jupyter_kernel_test.KernelTests):
 
@@ -243,11 +244,15 @@ def test_coq_jupyter____executing_code_with_undotted_separators____prints_evalua
             ("-", "-", ""),
             ("*", "*", ""),
             ("+", "+", ""),
-            ("{", "{", "}"),
-            ("1:{", "1 : {", "}"),
-            ("[G1]:{", "[ g2_' ] : {", "}"),
-            ("---", "---", "")
+            ("---", "---", ""),
         ]
+        if os.environ.get("LEGACY_COQ_VERSION", "0") == "0":
+            fixture += [
+                ("{", "{", "}"),
+                ("1:{", "1 : {", "}"),
+                ("[G1]:{", "[ g2_' ] : {", "}")
+            ]
+
         for (opening_separator1, opening_separator2, closing_separator) in fixture:
             (expected_results, commands) = zip(*[self._build_sum_command() for _ in range(4)])
             code = """
@@ -277,14 +282,13 @@ def test_coq_jupyter____executing_code_that_completes_subproof_while_having_unfo
         code = """
         Goal {0}={0} /\ {1}={1} /\ {2}={2}.
         split ; [ | split].
-        2:{{
-            easy.
+        - easy.
         """.format(marker1, marker2, marker3)
 
         result = self._execute_cell(code)
 
         self.assertIn("This subproof is complete, but there are some unfocused goals:", result, msg="Code:\n{}".format(code))
-        self.assertIn("{0} = {0}".format(marker1), result, msg="Code:\n{}".format(code))
+        self.assertIn("{0} = {0}".format(marker2), result, msg="Code:\n{}".format(code))
         self.assertIn("{0} = {0}".format(marker3), result, msg="Code:\n{}".format(code))
         self.assertNotIn("error", result.lower(), msg="Code:\n{}".format(code))