coq-par-compile: use hash for ancestors

[hendriktews]

The hash avoids an exponentially growing number of duplicates in
the ancestor collection. Fixes #499

[hendriktews]

Where can I find something about the test that is failing here?

[erikmd]

Hi @hendriktews, you can just click on the Checks tab of the PR.
But actually it seems the error is a spurious failure (the test 020_coq-test-definition fails with Coq 8.10 because at the time the assertion is checked, the expected text in *response* buffer is not there), so I guess we can just ignore that error!
(and I'll try to have a look on this later on to make the test more robust)

[erikmd]

@hendriktews albeit I'm not very elisp-hash-savvy, the PR LGTM and compiles fines… do you need that @RalfJung performs another test before the merge? or just when your patch will be available on MELPA.

[hendriktews]

Hi @hendriktews, you can just click on the Checks tab of the PR.

Yes, but there I only see that test (8.10, minimal) fails. Where can I find a description of the test that fails or its source code? Finding out that it is 020_coq-test-definition is already difficult, because this is somewhere hidden in the middle of the log.

I really appreciate that we have continuous integration now and even with automated tests! I am willing to investigate, when something fails on one of my RP's, but I don't really know how.

[hendriktews]

do you need that @RalfJung performs another test before the merge?

It would of course be nice, but I don't think it is required. I tested it on @RalfJung's repo and also tested it with an compilation error and coq-compile-keep-going...

[erikmd]

@hendriktews

Yes, but there I only see that test (8.10, minimal) fails. Where can I find a description of the test that fails or its source code? Finding out that it is 020_coq-test-definition is already difficult, because this is somewhere hidden in the middle of the log.
I really appreciate that we have continuous integration now and even with automated tests! I am willing to investigate, when something fails on one of my RP's, but I don't really know how.

Yes, the interface of GitHub Actions logs is not extremely intuitive, but to summarize:

• First click on the Checks tab − https://github.com/ProofGeneral/PG/pull/503/checks
• Click on the workflow name, CI (on the top-left of the Checks page, cf. screenshot below)
  
• You are now at page https://github.com/ProofGeneral/PG/actions/runs/141279705
• You can see the name of the tests that failed (cf. screenshot below)
  
• (If only one version of Coq is concerned, this might be a spurious failure)
• If need be, you can grep the test name in that file to get the code: https://github.com/ProofGeneral/PG/blob/master/ci/coq-tests.el
  

  PG/ci/coq-tests.el

  Lines 192 to 200 in 5cc2316

  	(ert-deftest 020_coq-test-definition ()
  	"Test *response* output after asserting a Definition."
  	(coq-fixture-on-file
  	(coq-test-full-path "test_stepwise.v")
  	(lambda ()
  	(coq-test-goto-before "(*test-definition*)")
  	(proof-goto-point)
  	(proof-shell-wait)
  	(coq-should-buffer-string "trois is defined"))))

• For further details, you can either:
  • Re-run the test locally in batch mode by doing cd .../PG/ci && ./test.sh (no docker binary required)
  • Re-run the test locally in interactive mode with − cf. New hook for early prompt/output analyzis. #495 (comment) :
    C-x C-f ci/coq-tests.el RETM-: (progn (load-file "coq-tests.el") (call-interactively #'ert)) RET
  • Or directly browse the GitHub Actions log, by clicking successively on:
    
    ↓
    
    ↓
    
    ↓
    
    (the main error line is automatically recognized (by a custom regexp) and underlined in red − this is the so-called Problem Matcher feature of GitHub Action)

[erikmd]

I tested it on @RalfJung's repo and also tested it with an compilation error and coq-compile-keep-going...

OK, thanks @hendriktews! 👍

So if no one objects, let's merge your PR on tomorrow Tuesday