Fail to establishes physical links to the external symbols #1115
Comments
|
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. |
|
Example: in your Makefile, add: |
|
PS. 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. |
This command return me an empty |
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 ?
The text was updated successfully, but these errors were encountered: