[README] [TUTORIAL] Error running dune build after changing paths

[tlringer]

After running make setup and then changing the paths, when I try to run dune build I get the following error I am not sure how to resolve:

(base) talia@xenon-v4:~/coq-synthesis$ dune build
File "./theories/Test.v", line 8, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 9, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 10, characters 0-27:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 43, in <module>
    from models.tactic_predictor import TacticPredictor
  File "/home/talia/proverbot9001-plugin/src/models/tactic_predictor.py", line 8, in <module>
    from data import (Dataset, RawDataset, ScrapedTactic, get_text_data,
  File "/home/talia/proverbot9001-plugin/src/data.py", line 40, in <module>
    from tokenizer import (Tokenizer,
  File "/home/talia/proverbot9001-plugin/src/tokenizer.py", line 33, in <module>
    from util import *
  File "/home/talia/proverbot9001-plugin/src/util.py", line 39, in <module>
    from dataloader import rust_parse_sexp_one_level
ModuleNotFoundError: No module named 'dataloader'
File "./theories/Test.v", line 23, characters 2-16:
Error:
System error: "search-report/trial-proofs.txt: No such file or directory"

Any idea what may be causing this?

[tlringer]

I think maybe it has something to do with these lines, which the coq-synthesis plugin doesn't do anything about: https://github.com/UCSD-PL/proverbot9001?tab=readme-ov-file#create-a-python-virtual-environment

[tlringer]

If I do that manually, and set the right environment, I now get this error instead:

(proverbot-env) (base) talia@xenon-v4:~/coq-synthesis$ dune build
File "./theories/Test.v", line 8, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 9, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 10, characters 0-27:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 416, in <module>
    main(sys.argv[1:])
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 73, in main
    predictor = get_predictor(parser, args)
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 192, in get_predictor
    predictor = loadPredictorByFile(args.weightsfile)
  File "/home/talia/proverbot9001-plugin/src/predict_tactic.py", line 114, in loadPredictorByFile
    predictor_type, saved_state = torch.load(str(filename), map_location='cpu')
  File "/home/talia/proverbot9001-plugin/proverbot-env/lib/python3.8/site-packages/torch/serialization.py", line 1040, in load
    return _legacy_load(opened_file, map_location, pickle_module, **pickle_load_args)
  File "/home/talia/proverbot9001-plugin/proverbot-env/lib/python3.8/site-packages/torch/serialization.py", line 1262, in _legacy_load
    magic_number = pickle_module.load(f, **pickle_load_args)
_pickle.UnpicklingError: invalid load key, '<'.
File "./theories/Test.v", line 23, characters 2-16:
Error:
System error: "search-report/trial-proofs.txt: No such file or directory"

[tlringer]

Looks to be a problem with the setup script not sourcing the conda env despite the command to do so being there. And then the second error is because I used a different Python version when following Proverbot9001's instructions on this. After talking to Arpan, I am trying to manually source the conda env before running dune build, and if that works we will probably update the instructions to make this the default.

[tlringer]

Now I get this error:

(synth) talia@xenon-v4:~/coq-synthesis$ dune build
File "./theories/Test.v", line 8, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 9, characters 0-17:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./theories/Test.v", line 10, characters 0-27:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 416, in <module>
    main(sys.argv[1:])
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 73, in main
    predictor = get_predictor(parser, args)
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 192, in get_predictor
    predictor = loadPredictorByFile(args.weightsfile)
  File "/home/talia/proverbot9001-plugin/src/predict_tactic.py", line 114, in loadPredictorByFile
    predictor_type, saved_state = torch.load(str(filename), map_location='cpu')
  File "/home/talia/.local/lib/python3.10/site-packages/torch/serialization.py", line 1040, in load
    return _legacy_load(opened_file, map_location, pickle_module, **pickle_load_args)
  File "/home/talia/.local/lib/python3.10/site-packages/torch/serialization.py", line 1262, in _legacy_load
    magic_number = pickle_module.load(f, **pickle_load_args)
_pickle.UnpicklingError: invalid load key, '<'.
File "./theories/Test.v", line 23, characters 2-16:
Error:
System error: "search-report/trial-proofs.txt: No such file or directory"

[tlringer]

Other projects that have similar errors point to the weights file being incorrect, so it would help to have a weights file to use that we know already works on someone else's computer, and see if that works.

[tlringer]

I tried pointing instead to this URL and it seems to be working now! Or at least, dune build is taking time now and so is probably trying to synthesize a proof rather than just giving up finding the weights at all.

So I guess there are two fixes that should come out of this:

1. In the Proverbot fork, point to these weights in the Makefile.
2. In the README and tutorial here, tell people to manually source the conda env, since the script doesn't appear to do that.

[tlringer]

How long is dune build supposed to take? I think the proof in Test.v is hard so it's relying on whatever the default timeout is to explore the whole search tree or something, and it has been hanging for almost 10 minutes now. Is that normal? In the default build it might be good to start with a proof we can synthesize quickly. Also it would be very nice to be able to tweak the timeout.

[tlringer]

I gave up since it didn't seem to be timing out. Trying to load something in an IDE to try instead, so I tried this line:

dune coq top --toplevel coqide tests/app_nil_r_test.v

And it just tells me that file doesn't exist even though it obviously does. (Also I don't think that step should be necessary if the build is doing a proper plugin installation, so I'm curious why it is needed.)

[tlringer]

OK, I moved that to theories and now that command works, but I'd like to look into why it's needed at all. But RunProverBot now seems to hang when I run it even inside of the app_nil_r_test file. Interestingly, if I give it the wrong file path, it prints that ProverBot ran successfully before complaining about not being able to find a file. So I think ProverBot is running and finding a proof, but that after that it is failing to open up a browser window or anything to show me results.

[tlringer]

Interestingly, I am getting error messages on the command line it looks like, even when it seems to be taking forever. Not sure what these mean, though:

Getting jobs: 100%|█████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 1/1 [00:00<00:00, 162.39it/s]
Searching proofs:   0%|                                                                                                                                                              | 0/1 [00:00<?, ?it/s]FAILED in file trial.v, lemma 
Theorem app_nil_r: forall {A: Type} (l: list A), l ++ [] = l.

Process Process-2:
Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 120, in addStmt
    self._update_state()
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 349, in _update_state
    self.cur_state = self._get_next_state()
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 358, in _get_next_state
    return match(normalizeMessage(msg),
  File "/home/talia/.local/lib/python3.10/site-packages/pampy/pampy.py", line 299, in match
    return run(action, lambda_args)
  File "/home/talia/.local/lib/python3.10/site-packages/pampy/pampy.py", line 48, in run
    return action(*var)
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 361, in <lambda>
    match(contents,
  File "/home/talia/.local/lib/python3.10/site-packages/pampy/pampy.py", line 299, in match
    return run(action, lambda_args)
  File "/home/talia/.local/lib/python3.10/site-packages/pampy/pampy.py", line 48, in run
    return action(*var)
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 366, in <lambda>
    else raise_(CoqExn("\n".join(searchStrsInMsg(rest)))),
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/coq_util.py", line 775, in raise_
    raise ex
coq_serapy.coq_backend.CoqExn: Syntax error: [unfold_occ] expected after 'unfold' (in [simple_tactic]).

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 275, in tryPrediction
    coq.run_stmt(prediction, timeout=min(time_left, time_per_command))
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/coq_agent.py", line 142, in run_stmt
    self._run_stmt_with_f(
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/coq_agent.py", line 152, in _run_stmt_with_f
    f(stm)
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/coq_agent.py", line 144, in <lambda>
    lambda stmt: self.backend.addStmt(
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 142, in addStmt
    self._handle_exception(e, stmt)
  File "/home/talia/proverbot9001-plugin/coq_serapy/src/coq_serapy/serapi_backend.py", line 500, in _handle_exception
    raise ParseError(f"Couldn't parse command {stmt}")
coq_serapy.coq_backend.ParseError: Couldn't parse command unfold fix.

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/talia/anaconda3/envs/synth/lib/python3.10/multiprocessing/process.py", line 315, in _bootstrap
    self.run()
  File "/home/talia/anaconda3/envs/synth/lib/python3.10/multiprocessing/process.py", line 108, in run
    self._target(*self._args, **self._kwargs)
  File "/home/talia/proverbot9001-plugin/src/search_file.py", line 248, in search_file_worker
    solution = worker.run_job(next_job, restart=not args.hardfail)
  File "/home/talia/proverbot9001-plugin/src/search_worker.py", line 250, in run_job
    attempt_search(self.args, job_lemma,
  File "/home/talia/proverbot9001-plugin/src/search_worker.py", line 356, in attempt_search
    result = dfs_proof_search_with_graph(lemma_name, module_prefix,
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 512, in dfs_proof_search_with_graph
    command_list, _ = search(pbar, [g.start_node], subgoals_stack_start, 0)
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 455, in search
    sub_search_result = search(pbar,
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 455, in search
    sub_search_result = search(pbar,
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 391, in search
    tryPrediction(args, coq, prediction.prediction,
  File "/home/talia/proverbot9001-plugin/src/search_strategies.py", line 277, in tryPrediction
    except (coq_serapy.TimeoutError, coq_serapy.ParseError,
AttributeError: module 'coq_serapy' has no attribute 'TimeoutError

Our updated TODO list now:

1. In the Proverbot fork, point to these weights in the Makefile.
2. In the README and tutorial here, tell people to manually source the conda env, since the script doesn't appear to do that.
3. Change Test.v to have a simple example that doesn't time out so that we can test the build on a very simple example.
4. Figure out how to get dune to properly install plugins rather than having to tell the IDE where to find the plugin.
5. Figure out the above issue---why the error exists to begin with.
6. Error handling, make sure the plugin doesn't hang when the model encounters an error.

[tlringer]

On the error above, Alex says:

There's a mismatch between your coq_serapy version and your Proverbot9001 version. Most of that backtrace is just "bad prediction", but that's supposed to be caught and counted as an error. But when it tries to catch it, it tries to import a symbol from coq_serapy that's been renamed, causing the crash. You'll need to figure out what commit of coq_serapy matches up to your Proverbot9001 branch, so that you can downgrade to that commit (I'm assuming it's a downgrade, and you accidentally pulled in a more recent version).

I think what we are seeing is that we generally have a versioning issue, where we rely on a fork of Proverbot with dependencies that were up-to-date when you set everything up, but that now have gotten out of sync and are no longer compatible. So the build either fails or gives you something that doesn't work because of the version changes. We need to make sure that everything we pull in here is versioned appropriately.

[tlringer]

Ah, on this one, you already had a fix in your branch of Proverbot9001, but I wasn't on the latest commit of that since I'd first tried to install this a while ago. So, to update the TODO list:

1. In the Proverbot fork, point to these weights in the Makefile.
2. In the README and tutorial here, tell people to manually source the conda env, since the script doesn't appear to do that.
3. Change Test.v to have a simple example that doesn't time out so that we can test the build on a very simple example.
4. Figure out how to get dune to properly install plugins rather than having to tell the IDE where to find the plugin.
5. Even if people have already installed your branch of Proverbot9001, make sure to pull the latest version of that in case things are out of sync.

[tlringer]

OK now the app_nil_r_test file succeeds! It gives me:

Proverbot ran successfully!
Here's the synthesized proof: 


Proof.
intros.
destruct l.
eauto.
simpl.
f_equal.
destruct l.
eauto.
intuition.
Qed.

However on the command line, I get an extra error:

/bin/sh: 1: alectryon: not found
Traceback (most recent call last):
  File "/home/talia/proverbot9001-plugin/src/create_webpage.py", line 40, in <module>
    main()
  File "/home/talia/proverbot9001-plugin/src/create_webpage.py", line 17, in main
    with open("proved_theorem.html") as fp:
FileNotFoundError: [Errno 2] No such file or directory: 'proved_theorem.html'

So that means our TODO list is now:

1. In the Proverbot fork, point to these weights in the Makefile.
2. In the README and tutorial here, tell people to manually source the conda env, since the script doesn't appear to do that.
3. Figure out why dune build runs Test.v and fails even when Test.v works in the IDE. (I can run Test.v in the IDE without issue.)
4. Figure out how to get dune to properly install plugins rather than having to tell the IDE where to find the plugin.
5. Even if people have already installed your branch of Proverbot9001, make sure to pull the latest version of that in case things are out of sync.
6. Make sure alectryon is installed correctly as part of the setup process. (I seem to have fixed this by using python3 -m pip rather than pip3.)
7. Generally check versioning issues. It looks like you changed this file to remove versions, but versioning is clearly needed here.

[tlringer]

And it works!!! (Added my fix to 6 above, and updated 3 since now Test.v works---but only in the IDE.) Lots to do to update instructions and build files and so on to make this usable though. Especially since upstream changes will continue to break this.

Now I will start to get it working on vscode as well, once I figure out how to get Coq working on VSCode, but if you can look at these 7 things in the meantime that'd be amazing.

[agrarpan]

Pushed changed that address TODO numbers 1, 2 and 5.
I'm not sure about 6 and 7.
Alectryon should be installed because its listed as a requirement in the .txt file.
And I removed versioning by removing the git submodule and adding a fixed set of files instead.
Will address number 3 soon.
Number 4 seems part of a bigger investigation and might require some additional time.