Use emacs --batch mode in agda-mode setup

[catern]

agda-mode setup should just run "emacs --batch" and have Emacs write the results of the query to stdout, instead of using a temporary file. Besides greatly simplifying the current askEmacs function, it would also work properly when running "agda-mode setup" without a terminal, which currently doesn't work.

(I would just make this patch myself but I can't figure out how to get agda building inside a Nix development shell)

[andreasabel]

The relevant code snippet is this:

agda/src/agda-mode/Main.hs

Lines 163 to 177 in 257a324

	askEmacs :: String -> IO String
	askEmacs query = do
	tempDir <- getTemporaryDirectory
	bracket (openTempFile tempDir "askEmacs")
	(removeFile . fst) $ \(file, h) -> do
	hClose h
	exit <- rawSystemWithDiagnostics "emacs"
	[ "--no-desktop", "-nw", "--no-splash"
	-- Andreas, 2014-01-11: ^ try a leaner startup of emacs
	-- Andreas, 2018-09-08: -nw instead of --no-window-system as some emacses do not support the long version
	, "--eval"
	, "(with-temp-file " ++ escape file ++ " "
	++ query ++ ")"
	, "--kill"
	]

Documentation of emacs --batch here: https://www.emacswiki.org/emacs/BatchMode

[andreasabel]

@catern, how does this work?

$ emacs --batch --eval "(expand-file-name user-init-file)"
Wrong type argument: stringp, nil

Maybe emacs in batch mode does not know about user-init-file?
Bingo!:

$ emacs --batch --eval="(print user-init-file)" 

nil

So, I suppose this does not work... Closing...

[catern]

Ah, that's true. If you pass --user='' to set init-file-user to an empty string then Emacs will load the init file normally:

emacs --user='' --batch --eval  '(princ (expand-file-name user-init-file))'

prints /home/catern/.emacs.d/init.el to stdout for me (no newline)

[andreasabel]

On my system, this prints extra garbage:

$ emacs --user='' --batch --eval '(print (expand-file-name user-init-file))' 2> /dev/null
#[nil "\300C\207"
      [t]
      1]

"/Users/abel/.emacs"

However, what currently is done in agda-mode works correctly:

$ emacs --user='' --batch --eval '(with-temp-file "foo.txt" (insert (expand-file-name user-init-file)))' 2> /dev/null
#[nil "\300C\207"
      [t]
      1]
$ cat foo.txt 
/Users/abel/.emacs

[catern]

Hm, that's weird, but it's definitely something that it's important to be tolerant of - a user's init file could do anything, including printing random stuff to standard-output. So I guess sticking with the temp-file is best.

It's still good to switch to --batch even though it doesn't simplify the implementation, because it allows agda-mode setup to be run without a terminal - e.g. M-& agda-mode setup inside Emacs, or ssh localhost agda-mode setup, will start working. (Also it avoids the momentary flicker of Emacs starting up)

[andreasabel]

I switch to --batch in

• Fix #5901: use --batch when installing agda-mode for emacs #5908

Please test!

[nad]

Please test!

The new code triggers a warning for me:

Warning (initialization): An error occurred while loading ‘[…]/.emacs’:

My current .emacs does not work properly together with --no-site-file. If we have to run the users' .emacs files, then I don't think we should use --no-site-file. However, the old code did not load .emacs, right?

An alternative might be to ensure that Emacs is run inside a terminal, but I don't know how to do that in a platform-independent way.

[andreasabel]

However, the old code did not load .emacs, right?

Well, I think it did: https://github.com/agda/agda/pull/5908/files#r881547737

But we can of course load the site file. Please test again:

• Re #5901: setup agda-mode: don't --no-site-file with --user #5919

[nad]

I manually ran code similar to what is in your pull request, and that seems to have worked.