Erik Martin-Dorel

> and maybe just add *programmatically in Lisp* a few more commands that are not state-preserving but which should be included in the whitelist. Typically, Time. For the record, after...

> I guess, we do not want to permit Focus for C-c C-v but we do want to omit proofs that contain Focus (if they don't contain other state changing...

> Therefore in https://github.com/ProofGeneral/PG/pull/694 function coq-cmd-prevents-proof-omission must first check for upper case. Was it really necessary? because AFAIK, **commands and tactics are kept apart in separate lists**.

> What do you think about distinguishing via STATECH commands that have > - no effect (eg. Show) > - proof local effect only (… e.g. Focus) > - global...

> That said the STATECH boolean has not been correctly maintained for a long time, and we don't rely much on it. Sure… but that does not look like a...

Thanks @Plictox! Note BTW: the standard convention for assignees in GitHub public repositories is generally as follows: → The developer that *implements* the feature (you) is the assignee of the...

Thanks @Rui00Barata for your contribution! We started discussed with @AltGr about your PR (just briefly for the time being), to sum up at this point: * it is not very...

Note: there are yet more warnings if we replace https://github.com/ocaml-sf/learn-ocaml/blob/8878c9b5557fb8ddc76aa3b68d03a25f06983a2d/Makefile#L4 with DUNE_ARGS = --root . --profile=dev --default-target @install

FWIW, there is a comprehensive example here: https://github.com/lsylvestre/easy-check/blob/master/easy-check/src/dune @AltGr this dune file doesn't have `(preprocess (action (run %{libexec:learn-ocaml.test_lib:grader-ppx} %{input-file})))` → is it a bug?

Hi. To install the latest release of opam on Ubuntu GNU/Linux, you can do: * `sudo apt-get remove opam` (to remove the old packaged version) * `curl -fL https://github.com/ocaml/opam/raw/master/shell/install.sh >...