issues with saving history to file

[Vincent Lefevre <vincent@xxxxxxxxxx>]

With zsh 5.9:

cventin:~> zsh -f
cventin% HISTFILE=~/.histfile
cventin% HISTSIZE=1000
cventin% SAVEHIST=1000
cventin% setopt APPEND_HISTORY
cventin% true
cventin% exit
cventin:~> ls ~/.histfile
ls: cannot access '/home/vlefevre/.histfile': No such file or directory

However, if I use INC_APPEND_HISTORY instead of APPEND_HISTORY, the
history is saved.

According to the zsh(1) man page:

  Note also that the RCS option affects the saving of history files,
  i.e. if RCS is unset when the shell exits, no history file will be
  saved.

But the difference between INC_APPEND_HISTORY and APPEND_HISTORY is
not documented concerning this point.

Also, I do not see the point of not saving the history when RCS is set.
IMHO, HISTFILE should just be unset by default; but if the user sets
this parameter, I suppose that the goal is to save the history.

Without INC_APPEND_HISTORY, the man page doesn't document when
precisely the history is saved. For instance, what happens if one
has a "print -s ..." in the .zlogout file?

Moreover, with INC_APPEND_HISTORY, "print -s" does not put the entry
in the history file immediately, only after the next accept-line.

-- 
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)