search

gpoesia / minimo

Learning Formal Mathematics from Intrinsic Motivation
MIT License
9 stars 7 forks source link

Running Experiment: "No module named 'domain'" Error #1

Closed khilling closed 1 month ago

khilling commented 1 month ago

Good evening,

When attempting to run the experiment using the command python .\bootstrap.py theory=groups, I encountered the following error: ModuleNotFoundError: No module named 'domain'. It appears that the domain module is not accessible from within minimo. I've verified that the module exists in peano but is not being detected.

Any insights or guidance would be greatly appreciated. Thank you!

gpoesia commented 1 month ago

Hi!

Sorry for the delay! The code indeed had a few remaining references to old code from the original Peano repository that are not used here. I just made a commit cleaning up some more of that, and was able to start a CPU run with bootstrap.py theory=groups. Let me know if that works for you now!

(I also realized I forgot to push the 'learning/theories' directory, where groups.p was... it's there now!).

khilling commented 1 month ago

Hello! Now it works for me. Thank you!