Stream: Coq devs & plugin devs

Topic: Tests giving different result on CI and local build


view this post on Zulip Ali Caglayan (Nov 10 2021 at 16:31):

@Emilio Jesús Gallego Arias What was the test that you mentioned in the call? It doesn't seem right that tests are differing in the CI and in local builds.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 16:41):

It fails in the dune+test_suite branch, here it is:

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 16:42):

cat _build/default/test-suite/unit-tests/printing/proof_diffs_test.ml.log
TEST SUCCEEDED: diff_str empty
TEST SUCCEEDED: diff_str white space
TEST SUCCEEDED: diff_str add/remove
TEST FAILED: tokenize_string/diff_mode in lexer (':=' is a single token
expected: true but got: false)
TEST SUCCEEDED: shorten_diff_span failure from #8922
TEST SUCCEEDED: diff_pp/add_diff_tags add/remove
TEST SUCCEEDED: diff_pp/add_diff_tags a span with spaces
TEST SUCCEEDED: diff_pp/add_diff_tags diff tags outside existing tags
TEST SUCCEEDED: diff_pp/add_diff_tags existing tagged values with spaces
TEST SUCCEEDED: diff_pp/add_diff_tags multiple tokens in pp
TEST SUCCEEDED: diff_pp/add_diff_tags token spanning multiple Ppcmd_strs
TEST SUCCEEDED: diff_pp/add_diff_tags empty string preserved
TEST SUCCEEDED: diff_hyps simple diffs
TEST SUCCEEDED: diff_hyps compacted
TEST SUCCEEDED: diff_hyps compacted with join
TEST SUCCEEDED: diff_hyps compacted with split
*** Ran 16 tests, with 15 successes and 1 failures ***
==========> FAILURE <==========
    test-suite/unit-tests/printing/proof_diffs_test.ml...Error!

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 16:48):

probably it didn't link g_constr

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 16:55):

Yup, that's my guess

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 16:55):

problem with linkall I mentioned


Last updated: Feb 02 2023 at 15:04 UTC