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.

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

enable Tramp support for Emacs 26 or later #569

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

hendriktews
Copy link
Collaborator

tramp support is not complete with these patches, but works if used with care. There are a few assertions that quick user interactions can trigger. Automatic background compilation via tramp is very slow, because tramp opens a new connection with all overhead for each asynchronous coqdep and coqc invocation. With these patches, tramp support only works for Emacs version 26 or later, because it uses make-nearby-temp-file.

This test exhibits a bug in background compilation that became
apparent when working on tramp support: Strange things may happen
when the user changes the current buffer, because part of the
code may then run with an incorrect default-directory.

Introduce hooks before and after busy waiting in the cct library.
tramp support is not complete with this patch, but works if used
with care. There are a few assertions that quick user
interactions can trigger. Automatic background compilation via
tramp is very slow, because tramp opens a new connection with all
overhead for each asynchronous coqdep and coqc invocation. With
this patch, tramp support only works for Emacs version 26 or
later, because it uses make-nearby-temp-file.

Modifications:
- switch to functions that properly deal with remote or magic files
- protect sentinels against multiple instances running
  interleaved, which suddenly happens under tramp
- recognize the error when coqdep cannot access a file

Fixes ProofGeneral#104 and fixes ProofGeneral#203.
@Matafou
Copy link
Contributor

Matafou commented Apr 11, 2022

FTR:

  • slowlyness was solved by @hendriktews (reusing tramp connexion)
  • the bug which triggers some assertion is still there as far as we can tell.

Merging now would need to warn users about not triggering any tramp feature during background compilation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants