Open NotBad4U opened 6 months ago
fblanqui
commented
6 months ago I suggest that you generate a file with lpo dependencies that you include in your Makefile (see #1108): it will be more optimal and may solve your problem (this is what I do in hol2dk). To generate dependencies, you can use a small script like https://github.com/Deducteam/hol2dk/blob/main/dep-lpo.
fblanqui
commented
6 months ago Example: in your Makefile, add:
include lpo.mk
LP_FILES := $(wildcard *.lp)
lpo.mk: $(LP_FILES:%.lp=%.lpo.mk)
find . -maxdepth 1 -name '*.lpo.mk' | xargs cat > $@
%.lpo.mk: %.lp
dep-lpo $*.lpPS. As you generate the lp files, it doesn't cost much to generate the .lpo.mk files as well at the same time, so that you don't need dep-lpo. This is what we do in hol2dk.
NotBad4U
commented
6 months ago Example: in your Makefile, add:
include lpo.mk LP_FILES := $(wildcard *.lp) lpo.mk: $(LP_FILES:%.lp=%.lpo.mk) find . -maxdepth 1 -name '*.lpo.mk' | xargs cat > $@ %.lpo.mk: %.lp dep-lpo $*.lpThis command return me an empty
lpo.mk. Could you explain to me what these commands are supposed to do? What should contain the lpo.mk and how I am supposed to use it? I understand that thedep-lposcript collect for a given lp file its list of requires and map into a list of*.lpo.
Hi !
I am working on a way to split my long proof into multiple files to check them across multiprocess. Each proof is cut into a segment that contains N symbols/steps of the proofs and there is a file that contains all the definitions. I wrote a simple Makefile like this that I want to run
make -j NHowever, the compilation of
.lpofails. Here is my trace:It failed because of this assert and looking at the code does not help me to much to understand what could be possible goes wrong. First, Make creates the .lpo for the file
axioms-0-10.lpand also compiledefinitions.lpbecause it requires it. Second, it try to create the .lpo foraxioms-10-20.lpand this time just loaddefinitions.lpobut I got this error. If I delete thedefinitions.lpoby hand and retry to run make then it work but fail again for the next segment (axioms-20-30.lp):any idea what could go wrong ?