search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
http://inf.fu-berlin.de/~lex/leo3
BSD 3-Clause "New" or "Revised" License
41 stars 10 forks source link

Using LEO-III as library and calling it repeatedly with different arguments leads to the changed arguments being ignored later calls #75

Open ColinRothgang opened 1 year ago

ColinRothgang commented 1 year ago

I'm currently testing a hammer tool (for MMT implemented here) that uses LEO-III as a library. As long as LEO-III is only used on one problem at a time this works without problems. However, when LEO-III's main method is called repeatedly with different (problem file path) arguments the main method seems to ignore the different arguments starting with the second call and uses the same arguments as in the first call to LEO-III.

I think this error originates from the way Configuration objects are initialized in LEO-III.

Concretely, I think the bug is here There the Configuration object is initialized from the arguments (given to the main method), whenever it isn't already initialized. However, when LEO-III is repeatedly called the Configuration object is initialized after the first call, meaning that the arguments passed starting with the second call to the main method will be ignored.

I understand that using LEO-III as a library is not the originally intended use case, nevertheless I think it would be worth it to change the initialization code to support repeated library calls to LEO-III as well.

lex-lex commented 12 months ago

Hi Colin, thanks for the pointer. Indeed, this is a known issue (to me) -- just as you said: Leo-III wasn't designed to be called via API but rather as a stand-alone executable. Looking back, this was not a smart decision :-)

I will have a look if some relatively simple changes could do the trick.

Best, Alex