search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

Broken in coq CI #146

Closed SkySkimmer closed 2 years ago

SkySkimmer commented 2 years ago

Last success https://gitlab.com/coq/coq/-/jobs/2930430501 First failure https://gitlab.com/coq/coq/-/jobs/2947461116

lukaszcz commented 2 years ago

PR https://github.com/coq/coq/pull/15220 broke CoqHammer's build system. I don't know why/how Coq's CI still worked with CoqHammer after that, but on my machine I could no longer build. The problem is with the lack of appropriate META.* files. Unfortunately, I couldn't find any documentation about them except basic usage, and my use-case is more involved (several packages/plugins which depend on each other). I couldn't figure out how to fix the coq_makefile-based build, so I switched to dune. It works locally on my computer and it works with Travis CI (https://github.com/lukaszcz/coqhammer/runs/8060215152). Why it doesn't work Coq's CI, I have no idea, and I'm not sure if I am capable of fixing this since I don't know how to debug Coq's CI directly. Maybe someone more familiar with dune / Coq's CI can take a brief look at it? The problem seems to be the command:

dune install coq-hammer-tactics
SkySkimmer commented 2 years ago

cc @gares

gares commented 2 years ago

what happened to the meta file added by https://github.com/lukaszcz/coqhammer/pull/115 ?

lukaszcz commented 2 years ago

Okay, I'm sorry for the confusion. This actually worked at that point with "make tactics && make install-tactics && make plugin". I had a different build process with "make" which I normally use but Coq's CI doesn't. That wasn't updated in #115 and it broke. I'll just revert to the previous state and remove the separate "make" build process.

lukaszcz commented 2 years ago

Though I would like to switch it to dune at some point. Unfortunately, the fact that it fails with the current Coq's CI for a reason I don't understand and can't reproduce prevents me from doing so.

SkySkimmer commented 2 years ago

Probably dune install puts stuff in the wrong place. For mathcomp-word we call it with --prefix="$CI_INSTALL_DIR".

lukaszcz commented 2 years ago

I think I've fixed it now