search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
488 stars 87 forks source link

Melpa fail to build #413

Open HuStmpHrrr opened 5 years ago

HuStmpHrrr commented 5 years ago

MELPA dist seems to fail on my machine. In particular, paths seem badly configured. For instance, all files in coq/ fail to compile if they have local dependencies, e.g. coq-syntax.el. If I compile this file, it generates the following messages.


Compiling file /home/hu/.emacs.d/elpa/proof-general-20181226.2300/coq/coq-syntax.el at Fri Jan  4 13:36:41 2019
Entering directory ‘/home/hu/.emacs.d/elpa/proof-general-20181226.2300/coq/’
coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db

I suppose something wrong with path config? I don't see code which add coq/ to load-path which explains this situation.

HuStmpHrrr commented 5 years ago

I upgraded to emacs 26.1 and this problem persists, so i guess it's a bug. I can see from the manual installation, load-path is twisted to make it work:

emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf
generic lib))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove
(quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile acl2/acl2.el

So I suppose it's a genuine bug.

erikmd commented 5 years ago

Hi @HuStmpHrrr, thanks for the report! I can reproduce this with a fresh Emacs 25.1 as follows:

$ git clone https://github.com/melpa/melpa
$ cd melpa
$ make clean-packages clean-sandbox recipes/proof-general sandbox

M-x package-install RET proof-general RET

and I get 13 errors:

coq-abbrev.el:23:1:Error: Cannot open load file: No such file or directory, coq-syntax
coq-compile-common.el:27:1:Error: Cannot open load file: No such file or directory, coq-system
coq-mode.el:28:1:Error: Cannot open load file: No such file or directory, coq-smie
coq-par-compile.el:39:1:Error: Cannot open load file: No such file or directory, coq-compile-common
coq-par-test.el:33:1:Error: Cannot open load file: No such file or directory, coq-par-compile
coq-seq-compile.el:30:1:Error: Cannot open load file: No such file or directory, coq-compile-common
coq-smie.el:43:1:Error: Cannot open load file: No such file or directory, coq-indent
coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db
coq-system.el:27:1:Error: Cannot open load file: No such file or directory, coq-mode
coq.el:54:1:Error: Cannot open load file: No such file or directory, coq-system
easycrypt-abbrev.el:14:1:Error: Cannot open load file: No such file or directory, easycrypt-syntax
easycrypt-syntax.el:14:1:Error: Cannot open load file: No such file or directory, easycrypt-keywords
easycrypt.el:15:1:Error: Cannot open load file: No such file or directory, easycrypt-syntax

I suspect this issue comes from the recent cleanup by @monnier but I did not investigate this further… This is a bit unfortunate as one of my courses in Toulouse should start using Emacs+PG from next Monday :/

Cc @ProofGeneral/core

monnier commented 5 years ago

I think I found the culprit. I just pushed a patch that should fix it.

erikmd commented 5 years ago

Excellent! thank you Stefan for the prompt fix :+1: I have redone the steps mentioned in my comment and it seems very OK. I guess we can close that issue. @HuStmpHrrr please reopen if ever the fix were not working with your version of emacs.

erikmd commented 5 years ago

Hi @monnier @cpitclaudel, FYI Stefan's fix 58cea1b8ffb02bc546ddb56a669d4094390d4809 was not enough to make proof-general.el work in all situations (in particular with this proposed procedure, where use-package + proof-general are installed at ~/.emacs first load, I was still getting 13 bytecomp errors). I made many intermediate tweaks between the "broken" version in master and 05df29f7ff065d8da45b81691c602b6cf075e4a0, which was working. Finally, I restored Clément's original code of pg-init.el :smiley: (renamed to proof-general.el) and it now seems to work smoothly with use-package. (But feel free to comment if you have an explanation of what was going on there…) Kind regards, Erik

HuStmpHrrr commented 5 years ago

I installed PG from melpa again and it worked.

thirs commented 2 years ago

This issue seems to have reappeared on my computer:

Compiling file /home/thirs/.emacs.d/elpa/proof-general-20220310.2253/coq/coq-syntax.el at Mon Mar 28 18:04:38 2022 coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db Does anyone have any hints?

It looks like the above-described patch has been un-applied...

Matafou commented 2 years ago

Hi. Bad news :-(. @erikmd, do you think we can add the special build of the melpa package as a test in our CI?

Matafou commented 2 years ago

@thirs can you describe the procedure to obtain this error? Is it when installing the elpa package?

thirs commented 2 years ago

Yes, I think I just installed it via melpa, followed the "quick installation instructions" on the website, and tried to open some ".v" file. I then tried with a fresh .emacs. I'll try again on a different computer today.

thirs commented 2 years ago

@Matafou It seems to work out of the box on the other computer.

thirs ~ $ emacs --version
GNU Emacs 27.1
Copyright (C) 2020 Free Software Foundation, Inc.
GNU Emacs comes with ABSOLUTELY NO WARRANTY.
You may redistribute copies of GNU Emacs
under the terms of the GNU General Public License.
For more information about these matters, see the file named COPYING.
thirs ~ $ uname -a
Linux lama-e29 5.10.0-10-amd64 #1 SMP Debian 5.10.84-1 (2021-12-08) x86_64 GNU/Linux
thirs ~ $ coqtop --version
The Coq Proof Assistant, version 8.12.0 (November 2020)
compiled on Nov 25 2020 6:34:32 with OCaml 4.11.1

Previous computer had the same except for Debian 5.10.103-1 (2022-03-07).

thirs commented 2 years ago

@Matafou I forgot to look up the version numbers of the elpa package: on the first machine it was 20220310.2253, while it is 20220328.1209 on the other. So I tried the newer version on the first machine, and it also doesn't work.

So I guess it has to do with emacs configuration, right? What should I look for?

On today's computer, melpa says

  async              20191009.1018 installed             Asynchronous processing in Emacs
  auctex             12.1.1        installed             Integrated environment for *TeX*
  bind-key           20210210.1609 installed             A simple way to manage personal keybindings
  company-coq        20220314.526  installed             A collection of extensions for Proof General's Coq mode
  exec-path-from-shell 20210914.1247 installed             Get environment variables such as $PATH from the shell
  list-utils         20160414.702  installed             List-manipulation utility functions
  math-symbol-lists  1.1           installed             Lists of Unicode math symbols and latex commands
  proof-general      20220328.1209 installed             A generic Emacs interface for proof assistants
  ucs-utils          20150826.714  installed             Utilities for Unicode characters
  use-package        20210207.1926 installed             A configuration macro for simplifying your .emacs
  company            20180501.11   dependency            Modular text completion framework
  company-math       1.1           dependency            Completion backends for unicode math symbols and latex tags
  dash               20180413.30   dependency            A modern list library for Emacs
  pcache             20170105.1414 dependency            persistent caching for Emacs.
  persistent-soft    20150223.1053 dependency            Persistent storage, returning nil on failure
  yasnippet          20180412.1548 dependency            Yet another snippet extension for Emacs.
  notmuch            0.35          external              Emacs based front-end (MUA) for notmuch
  allout             2.3           built-in              extensive outline mode for use alone and with other modes
  allout-widgets     1.0           built-in              Visually highlight allout outline structure.
  ansi-color         3.4.2         built-in              translate ANSI escape sequences into faces
  antlr-mode         2.2.3         built-in              major mode for ANTLR grammar files
  artist             1.2.6         built-in              draw ascii graphics with your mouse
  auth-source-pass   5.0.0         built-in              Integrate auth-source with password-store
  backtrace          1.0           built-in              generic major mode for Elisp backtraces
  bs                 1.17          built-in              menu for selecting and displaying buffers
  cc-mode            5.33.1        built-in              user customization variables for CC Mode
  cedet              2.0           built-in              Data structure debugger
  cfengine           1.4           built-in              mode for editing Cfengine files
  chart              0.2           built-in              Draw charts (bar charts, etc)
  checkdoc           0.6.2         built-in              check documentation strings for style requirements
  cl-generic         1.0           built-in              CLOS-style generic functions for Elisp
  cl-lib             1.0           built-in              Common Lisp extensions for Emacs
  cl-print           1.0           built-in              CL-style generic printing
  cwarn              1.3.1         built-in              highlight suspicious C and C++ constructions
  delim-col          2.1           built-in              prettify all columns in a region or rectangle
  dunnet             2.2           built-in              text adventure for Emacs
  ebnf2ps            4.4           built-in              translate an EBNF to a syntactic chart on PostScript
  ede                1.2           built-in              EDE utilities
  ediff              2.81.6        built-in              a comprehensive visual interface to diff & patch
  edmacro            2.1           built-in              keyboard macro editor
  eieio              1.4           built-in              Enhanced Implementation of Emacs Interpreted Objects
  eieio-core         1.4           built-in              Core implementation for eieio
  epg                1.0.0         built-in              the EasyPG Library
  erc                5.3           built-in              An Emacs Internet Relay Chat client
  eshell             2.4.2         built-in              the Emacs command shell
  faceup             0.0.6         built-in              Markup language for faces and font-lock regression testing
  feedmail           11            built-in              assist other email packages to massage outgoing messages
  find-cmd           0.6           built-in              Build a valid find(1) command with sexps
  finder             1.0           built-in              topic & keyword-based code finder
  flymake            1.0.8         built-in              A universal on-the-fly syntax checker
  flymake-proc       1.0           built-in              Flymake backend for external tools
  foldout            1.10          built-in              folding extensions for outline-mode and outline-minor-mode
  footnote           0.19          built-in              footnote support for message mode
  gamegrid           1.2           built-in              library for implementing grid-based games on Emacs
  gnus               5.13          built-in              Identifying spam
  hippie-exp         1.6           built-in              expand text trying various ways to find its expansion
  htmlfontify        0.21          built-in              htmlize a buffer/source tree with optional hyperlinks
  icalendar          0.19          built-in              iCalendar implementation
  idlwave            6.1.22        built-in              IDL editing mode for GNU Emacs
  image-dired        0.4.11        built-in              use dired to browse and manipulate your images
  info-xref          3             built-in              check external references in an Info document
  inversion          1.3           built-in              When you need something in version XX.XX
  isearchb           1.5           built-in              a marriage between iswitchb and isearch
  js                 9             built-in              Major mode for editing JavaScript
  json               1.4           built-in              JavaScript Object Notation parser / generator
  jsonrpc            1.0.9         built-in              JSON-RPC library
  let-alist          1.0.6         built-in              Easily let-bind values of an assoc-list by their names
  linum              0.9.24        built-in              display line numbers in the left margin
  map                2.0           built-in              Map manipulation functions
  master             1.0.2         built-in              make a buffer the master over another buffer
  md4                1.0           built-in              MD4 Message Digest Algorithm.
  meta-mode          1.0           built-in              major mode for editing Metafont or MetaPost sources
  mh-e               8.6snapshot   built-in              MH-E X-Face and Face header field display
  mixal-mode         0.1           built-in              Major mode for the mix asm language.
  nadvice            1.0           built-in              Light-weight advice primitives for Elisp functions
  ntlm               2.1.0         built-in              NTLM (NT LanManager) authentication support
  org                9.3           built-in              Export Framework for Org Mode
  package            1.1.0         built-in              Simple package system for Emacs
  printing           6.9.3         built-in              printing utilities
  ps-mode            1.1.9         built-in              PostScript mode for GNU Emacs
  ps-print           7.3.5         built-in              ps-print sample setup code
  pulse              1.0           built-in              Pulsing Overlays
  python             0.26.1        built-in              Python's flying circus support for Emacs
  regi               1.8           built-in              REGular expression Interpreting engine
  remember           2.0           built-in              a mode for quickly jotting down things to remember
  repeat             0.51          built-in              convenient way to repeat the previous command
  ruby-mode          1.2           built-in              Major mode for editing Ruby files
  ruler-mode         1.6           built-in              display a ruler in the header line
  sasl               1.0           built-in              SASL client framework
  savehist           24            built-in              Save minibuffer history
  semantic           2.2           built-in              GNU Bison for Emacs - Runtime
  seq                2.21          built-in              Sequence manipulation functions
  sh-script          2.0.6         built-in              shell-script editing commands for Emacs
  so-long            1.0           built-in              Say farewell to performance problems with minified code.
  soap-client        3.1.5         built-in              Interactive WSDL inspector
  sql                3.6           built-in              specialized comint.el for SQL interpreters
  srecode            1.2           built-in              Srecode texinfo support.
  svg                1.0           built-in              SVG image creation functions
  tabulated-list     1.0           built-in              generic major mode for tabulated lists
  tetris             2.1           built-in              implementation of Tetris for Emacs
  thunk              1.0           built-in              Lazy form evaluation
  tildify            4.6.1         built-in              adding hard spaces into texts
  timeclock          2.6.1         built-in              mode for keeping track of how much you work
  tramp              2.4.3         built-in              Transparent Remote Access, Multiple Protocol
  vera-mode          2.28          built-in              major mode for editing Vera files
  verilog-mode       2019.12.17.268053413 built-in              major mode for editing verilog source in Emacs
  viper              3.14.1        built-in              A full-featured Vi emulator for Emacs
  wdired             2.0           built-in              Rename files editing their names in dired buffers
  whitespace         13.2.2        built-in              minor mode to visualize TAB, (HARD) SPACE, NEWLINE
  woman              0.551         built-in              browse UN*X manual pages `wo (without) man'

On yesterday's computer (on which it doesn't work), it says:

  auctex             13.1.1        installed             Integrated environment for *TeX*
  bind-key           20210210.1609 installed             A simple way to manage personal keybindings
  company-coq        20220314.526  installed             A collection of extensions for Proof General's Coq mode
  company-try-hard   20200417.1603 installed             get all completions from company backends
  elm-mode           20220227.931  installed             Major mode for Elm
  exec-path-from-shell 20210914.1247 installed             Get environment variables such as $PATH from the shell
  ghub               20220325.1028 installed             Minuscule client libraries for Git forge APIs.
  latex-unicode-math-mode 20170123.1816 installed             Input method for Unicode math symbols
  let-alist          1.0.6         installed             Easily let-bind values of an assoc-list by their names
  list-utils         20210111.1522 installed             List-manipulation utility functions
  math-symbol-lists  20200131.2338 installed             Lists of Unicode math symbols and latex commands
  modus-themes       20220329.442  installed             Elegant, highly legible and customizable themes
  peg                20150708.641  installed             Parsing Expression Grammars in Emacs Lisp
  proof-general      20220328.1209 installed             A generic Emacs interface for proof assistants
  ucs-utils          20150826.1414 installed             Utilities for Unicode characters
  use-package        20210207.1926 installed             A configuration macro for simplifying your .emacs
  w3m                20211122.335  installed             an Emacs interface to w3m
  zotelo             20160602.949  installed             Manage Zotero collections from emacs
  ztree              20210415.1947 installed             Text mode directory tree
  company            20220328.155  dependency            Modular text completion framework
  company-math       20210731.2019 dependency            Completion backends for unicode math symbols and latex tags
  dash               20210826.1149 dependency            A modern list library for Emacs
  f                  20210624.1103 dependency            Modern API for working with files and directories
  pcache             20201226.634  dependency            persistent caching for Emacs.
  persistent-soft    20150223.1853 dependency            Persistent storage, returning nil on failure
  reformatter        20210831.1405 dependency            Define commands which run reformatters on the current buffer
  s                  20210616.619  dependency            The long lost Emacs string manipulation library.
  seq                2.23          dependency            Sequence manipulation functions
  treepy             20191108.2217 dependency            Generic tree traversal tools
  yasnippet          20200604.246  dependency            Yet another snippet extension for Emacs
  caml               4.6           external              OCaml code editing commands for Emacs
  dash               2.17.0        external              A modern list library for Emacs
  dash-functional    1.2.0         external              Collection of useful combinators for Emacs Lisp
  epl                0.9           external              Emacs Package Library
  git-commit         2.99.0        external              Edit Git commit messages
  haskell-mode       17.2snapshot  external              A Haskell editing mode
  htmlize            1.55          external              Convert buffer text and decorations to HTML.
  magit-popup        2.13.2        external              Define prefix-infix-suffix command combos
  org                9.4           external              Outline-based notes management and organizer
  transient          0.2.0.30      external              Emacs key and popup interface for complex keybindings
  tuareg             2.2.0         external              OCaml mode for Emacs.
  with-editor        3.0.2         external              Use the Emacsclient as $EDITOR
  allout             2.3           built-in              extensive outline mode for use alone and with other modes
  allout-widgets     1.0           built-in              Visually highlight allout outline structure.
  ansi-color         3.4.2         built-in              translate ANSI escape sequences into faces
  antlr-mode         2.2.3         built-in              major mode for ANTLR grammar files
  artist             1.2.6         built-in              draw ascii graphics with your mouse
  auth-source-pass   5.0.0         built-in              Integrate auth-source with password-store
  backtrace          1.0           built-in              generic major mode for Elisp backtraces
  bs                 1.17          built-in              menu for selecting and displaying buffers
  cc-mode            5.33.1        built-in              user customization variables for CC Mode
  cedet              2.0           built-in              Data structure debugger
  cfengine           1.4           built-in              mode for editing Cfengine files
  chart              0.2           built-in              Draw charts (bar charts, etc)
  checkdoc           0.6.2         built-in              check documentation strings for style requirements
  cl-generic         1.0           built-in              CLOS-style generic functions for Elisp
  cl-lib             1.0           built-in              Common Lisp extensions for Emacs
  cl-print           1.0           built-in              CL-style generic printing
  cwarn              1.3.1         built-in              highlight suspicious C and C++ constructions
  delim-col          2.1           built-in              prettify all columns in a region or rectangle
  dunnet             2.2           built-in              text adventure for Emacs
  ebnf2ps            4.4           built-in              translate an EBNF to a syntactic chart on PostScript
  ede                1.2           built-in              EDE utilities
  ediff              2.81.6        built-in              a comprehensive visual interface to diff & patch
  edmacro            2.1           built-in              keyboard macro editor
  eieio              1.4           built-in              Enhanced Implementation of Emacs Interpreted Objects
  eieio-core         1.4           built-in              Core implementation for eieio
  epg                1.0.0         built-in              the EasyPG Library
  erc                5.3           built-in              An Emacs Internet Relay Chat client
  eshell             2.4.2         built-in              the Emacs command shell
  faceup             0.0.6         built-in              Markup language for faces and font-lock regression testing
  feedmail           11            built-in              assist other email packages to massage outgoing messages
  find-cmd           0.6           built-in              Build a valid find(1) command with sexps
  finder             1.0           built-in              topic & keyword-based code finder
  flymake            1.0.8         built-in              A universal on-the-fly syntax checker
  flymake-proc       1.0           built-in              Flymake backend for external tools
  foldout            1.10          built-in              folding extensions for outline-mode and outline-minor-mode
  footnote           0.19          built-in              footnote support for message mode
  gamegrid           1.2           built-in              library for implementing grid-based games on Emacs
  gnus               5.13          built-in              Identifying spam
  hippie-exp         1.6           built-in              expand text trying various ways to find its expansion
  htmlfontify        0.21          built-in              htmlize a buffer/source tree with optional hyperlinks
  icalendar          0.19          built-in              iCalendar implementation
  idlwave            6.1.22        built-in              IDL editing mode for GNU Emacs
  image-dired        0.4.11        built-in              use dired to browse and manipulate your images
  info-xref          3             built-in              check external references in an Info document
  inversion          1.3           built-in              When you need something in version XX.XX
  isearchb           1.5           built-in              a marriage between iswitchb and isearch
  js                 9             built-in              Major mode for editing JavaScript
  json               1.4           built-in              JavaScript Object Notation parser / generator
  jsonrpc            1.0.9         built-in              JSON-RPC library
  let-alist          1.0.6         built-in              Easily let-bind values of an assoc-list by their names
  linum              0.9.24        built-in              display line numbers in the left margin
  map                2.0           built-in              Map manipulation functions
  master             1.0.2         built-in              make a buffer the master over another buffer
  md4                1.0           built-in              MD4 Message Digest Algorithm.
  meta-mode          1.0           built-in              major mode for editing Metafont or MetaPost sources
  mh-e               8.6snapshot   built-in              MH-E X-Face and Face header field display
  mixal-mode         0.1           built-in              Major mode for the mix asm language.
  nadvice            1.0           built-in              Light-weight advice primitives for Elisp functions
  ntlm               2.1.0         built-in              NTLM (NT LanManager) authentication support
  org                9.3           built-in              Export Framework for Org Mode
  package            1.1.0         built-in              Simple package system for Emacs
  printing           6.9.3         built-in              printing utilities
  ps-mode            1.1.9         built-in              PostScript mode for GNU Emacs
  ps-print           7.3.5         built-in              ps-print sample setup code
  pulse              1.0           built-in              Pulsing Overlays
  python             0.26.1        built-in              Python's flying circus support for Emacs
  regi               1.8           built-in              REGular expression Interpreting engine
  remember           2.0           built-in              a mode for quickly jotting down things to remember
  repeat             0.51          built-in              convenient way to repeat the previous command
  ruby-mode          1.2           built-in              Major mode for editing Ruby files
  ruler-mode         1.6           built-in              display a ruler in the header line
  sasl               1.0           built-in              SASL client framework
  savehist           24            built-in              Save minibuffer history
  semantic           2.2           built-in              GNU Bison for Emacs - Runtime
  seq                2.21          built-in              Sequence manipulation functions
  sh-script          2.0.6         built-in              shell-script editing commands for Emacs
  so-long            1.0           built-in              Say farewell to performance problems with minified code.
  soap-client        3.1.5         built-in              Interactive WSDL inspector
  sql                3.6           built-in              specialized comint.el for SQL interpreters
  srecode            1.2           built-in              Srecode texinfo support.
  svg                1.0           built-in              SVG image creation functions
  tabulated-list     1.0           built-in              generic major mode for tabulated lists
  tetris             2.1           built-in              implementation of Tetris for Emacs
  thunk              1.0           built-in              Lazy form evaluation
  tildify            4.6.1         built-in              adding hard spaces into texts
  timeclock          2.6.1         built-in              mode for keeping track of how much you work
  tramp              2.4.3         built-in              Transparent Remote Access, Multiple Protocol
  vera-mode          2.28          built-in              major mode for editing Vera files
  verilog-mode       2019.12.17.268053413 built-in              major mode for editing verilog source in Emacs
  viper              3.14.1        built-in              A full-featured Vi emulator for Emacs
  wdired             2.0           built-in              Rename files editing their names in dired buffers
  whitespace         13.2.2        built-in              minor mode to visualize TAB, (HARD) SPACE, NEWLINE
  woman              0.551         built-in              browse UN*X manual pages `wo (without) man'
  proof-general      20220328.1209 obsolete              A generic Emacs interface for proof assistants

Weird: proof-general is there twice, once as installed, once as obsolete, with the same version. But installation failed so I guess this is more a consequence of the failure than a cause.

Matafou commented 2 years ago

Weird: proof-general is there twice, once as installed, once as obsolete, with the same version. But installation failed so I guess this is more a consequence of the failure than a cause.

You sure you don't have any other remaining part from an older installation of proofgeneral? I can't reproduce here (emacs 27.1).

thirs commented 2 years ago

Not entirely, but 

thirs ~ $ locate proof | grep general
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/AUTHORS
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/CHANGES
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/COPYING
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/PG-adapting.info
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/ProofGeneral.info
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/coq

seems do say so.

Matafou commented 2 years ago

I tried this and I do not see any problem.

$ git clone https://github.com/melpa/melpa
$ cd melpa
$ make clean-packages clean-sandbox recipes/proof-general sandbox
M-x package-install RET proof-general RET

@erikmd @monnier do you have any clue?