Make output test-suite robust against passing absolute paths to coqc

[JasonGross]

In order to effectively minimize developments from Coq's CI, I need to absolutize paths before passing them to coqc so that I can recognize which error message the file occurs in. (I can't think of any robust way to find the relevant file without absolutizing the paths.) However, this wrapping of coqc breaks HB's test-suite with the error message

--- tests/about.v.out	2021-06-14 14:04:42.000000000 +0000
+++ tests/about.v.out.aux	2021-06-29 14:44:05.213142936 +0000
@@ -114,11 +114,11 @@
     - hierarchy_5.AddMonoid
       hierarchy_5.AddComoid
       hierarchy_5.AddAG
-      (from "./tests/about.v", line 5)
+      (from "/github/workspace/builds/coq/coq-passing/_build_ci/hierarchy_builder/tests/about.v", line 5)
     - hierarchy_5.BiNearRing
       hierarchy_5.SemiRing
       hierarchy_5.Ring
-      (from "./tests/about.v", line 10)
+      (from "/github/workspace/builds/coq/coq-passing/_build_ci/hierarchy_builder/tests/about.v", line 10)
 
 HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
     hierarchy_5.Ring to hierarchy_5.SemiRing
@@ -131,4 +131,4 @@
 HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to 
 hierarchy_5.BiNearRing_of_AddMonoid
 HB: synthesized in file 
-./tests/about.v, characters 120-242, line 5, column 122
+/github/workspace/builds/coq/coq-passing/_build_ci/hierarchy_builder/tests/about.v, characters 120-242, line 5, column 122
Makefile.test-suite.coq.local:4: recipe for target 'post-all' failed

Could you adapt the test-suite so that the output tests don't depend on whether the files are called with relative paths or absolute paths, so that I can support minimizing CI developments that depend on HB?

[gares]

I think this is already fixed here https://github.com/math-comp/hierarchy-builder/pull/252/files?file-filters%5B%5D=.opam#diff-907ddde5421afcf185d3897a9d23d389ff87d6bec6b5dd03d1a0cd6dc31af60f (yet to be merged in master)

[JasonGross]

How does that PR fix the issue? As far as I can tell, the file name will still be reported with the path that was passed to coqc, and hence my minor alteration of the build process to always pass absolute paths to coqc will break the output test.

[gares]

The makefile has two targets: build and tests. Make all does both. The opam package will stop invoking tests unless you call opam with --with-test.

[gares]

How do you build HB?

[JasonGross]

I mv coqc coqc.orig, and then create a bash file named coqc that parses the arguments and absolutizes file names, before passing them on to coqc.orig. Then I invoke make -f Makefile.ci GITLAB_CI=1 ci-elpi in a clone of Coq, as is done on Coq's own CI.

[JasonGross]

(The coqc wrapper that I write also prints its arguments as well as COQPATH to stderr; this is the only robust and reliable way I've found to parse the arguments to coqc and the relevant env from the log of make -f Makefile.ci GITLAB_CI=1 ci-elpi, and to be able to find the correct file based on Coq's error message in the log.)

[JasonGross]

This issue showed up again at coq/coq#14798 (comment), is there a way to fix this?