Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

missing dependency in fmdev.el #1

Open
aa755 opened this issue Feb 13, 2025 · 3 comments · May be fixed by #3
Open

missing dependency in fmdev.el #1

aa755 opened this issue Feb 13, 2025 · 3 comments · May be fixed by #3

Comments

@aa755
Copy link

aa755 commented Feb 13, 2025

when I delete _build, and open emacs and do proof-goto-point, I get some vfork: file not found error, even if dune coq top file.v has already been called. the problem goes away on doing full dune build. can fmdev.el ask dune to build whatever it needs?
@Blaisorblade
Copy link
Contributor

So, you delete _build, call dune coq top file.v, then loading a file fails even if you restart Emacs?
Can you confirm that running dune b _build/default/fmdeps/coq/dev/shim/coqtop is enough to fix the problem? If that's not, dune b @fmdeps/coq/install should suffice? This is part of fm-build.py -u, which is used sometimes in support/bedrock.el (internal-only right now).

It seems fmdev.el skips dune entirely right now. I'll ask Simon.

@cipher1024
Copy link

Sometimes I need to rerun fmdev.el manually when starting a new instance of emacs. I haven't found what the reason is. If that's not the right fix, usually what @Blaisorblade suggests does the trick for me.

@aa755
Copy link
Author

aa755 commented Mar 5, 2025

So, you delete _build, call dune coq top file.v, then loading a file fails even if you restart Emacs?

Yes.

Can you confirm that running dune b _build/default/fmdeps/coq/dev/shim/coqtop is enough to fix the problem?

Yes, that works.

It seems fmdev.el skips dune entirely right now. I'll ask Simon.

Yes, ideally, fmdev.el should call dune b _build/default/fmdeps/coq/dev/shim/coqtop after finding the project root for the current file. We can leave this issue open in case one of us gets a chance to implement that.

@aa755 aa755 linked a pull request Mar 5, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fmdev.el: build coqtop before returing a reference to it aa755/fm-workspace
3 participants
@cipher1024 @Blaisorblade @aa755