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

fix(emacs): only use vfiles in etags action #1764

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Sep 18, 2023

@jdchristensen This should work better.

dune Outdated Show resolved Hide resolved
@jdchristensen
Copy link
Collaborator

This still has the extra quoting around the regular expression arguments. This is how I see the command

rm -f TAGS _build/default/TAGS; dune build --verbose --cache=disabled -f --always-show-command-line TAGS

and in a correctly built TAGS file, grep functor_join TAGS should show output.

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

@jdchristensen The command that dune outputs with --verbose and --always-show-command-line isn't always accurate, especially when it comes to quoting. I will play around with etags myself to see what might be going wrong.

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

The reason I say that is because I wrote my own etags executable in order to echo out the arguments being passed:

Argument 1: ../install/default/bin/etags
Argument 2: --language=none
Argument 3: -r '/^[ \t]*\(\(Local\|Global\|Cumulative\|NonCumulative\|Monomorphic\|Polymorphic\|Private\)[ \t]+\)*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Inductive\|CoInductive\|Proposition\)[ \t]+\([a-zA-Z0-9_'\'']+\)/\4/'
Argument 4: -r '/^[ \t]*\([a-zA-Z0-9_'\'']+\)[ \t]*:/\1/'
Argument 5: theories/Algebra/AbGroups.v
Argument 6: theories/Algebra/AbGroups/AbHom.v
Argument 7: theories/Algebra/AbGroups/AbProjective.v
Argument 8: theories/Algebra/AbGroups/AbPullback.v
Argument 9: theories/Algebra/AbGroups/AbPushout.v

It looks to me as the regex is being passed fine. The quotation you see is an artefact of how dune serialises its internal commands to shell commands.

@Alizter Alizter force-pushed the ps/branch/fix_emacs___only_use_vfiles_in_etags_action branch from f322ea1 to 401f0e5 Compare September 18, 2023 20:53
@jdchristensen
Copy link
Collaborator

No, what etags is getting as "Argument 3" is supposed to be two arguments. The quoting that dune inserts combines them into one argument. But maybe just inserting line breaks in the etags-args file would fix it?

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

OK I've managed to fix it. The issue is that we were running the etags program directly essentially using the unix exec. The shell scripting magic that was being done is actually quite essential before being passed into etags. Therefore switching the action to use the (system) shell fixes the issues. I've checked by hand and dune and make agree here.

@jdchristensen
Copy link
Collaborator

jdchristensen commented Sep 18, 2023

Also, Argument 3 has some single quote characters in it that shouldn't be there.

@Alizter Alizter force-pushed the ps/branch/fix_emacs___only_use_vfiles_in_etags_action branch from 401f0e5 to fe44956 Compare September 18, 2023 20:57
@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

I've also removed the %{bin:etags} from the deps and put it directly in the (system) action. Dune will automatically add the dependency there so we don't need to be explicit about it. This also allows us to avoid having to bind a name to a subset of the deps and go back to using %{deps}.

@jdchristensen Can you give this push a go?

@jdchristensen
Copy link
Collaborator

This seems to be working, but I don't see how. There are still extra single quote characters being passed to etags, which should mess it up. It must have some internal code that deletes them. But I think it would be cleaner to not rely on this behaviour. Can dune literally put the contents of a file on the command line? If not, maybe it's cleaner to put the etags command and its args into a script?

@jdchristensen
Copy link
Collaborator

I can try the script method if dune can't create the right command line.

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

@jdchristensen The removal of the quote characters is standard shell expansion (i.e. what happens when you shove that expression thorugh sh or bash). This is the same behaviour that the makefile relies on. Feel free to remove any shell behaviours if they are not to your liking. I don't mind keeping them in for something like TAGS however.

@jdchristensen
Copy link
Collaborator

@Alizter I'm going to PR a different method that I think is easier to understand. You can let me know what you think.

@Alizter Alizter closed this Sep 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants