diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/change-header | 21 | ||||
| -rw-r--r-- | dev/tools/coqdev.el | 35 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 32 |
3 files changed, 39 insertions, 49 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header index 687c02f4f1..59c6f43958 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -13,22 +13,19 @@ newheader=$2 if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi -n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` -nsucc=`expr $n + 1` - -linea='(* -*- coding:utf-8 -*- *)' -lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' +n=$(wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g") +nsucc=$(expr $n + 1) modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do - headline=`head -n 1 $i` - if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then - # Has emacs header +for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do + headline=$(head -n 1 $i) + if $(echo $headline | grep "(\* -\*- .* \*)" > /dev/null) || $(echo $headline | grep "^#\!" > /dev/null); then + # Has header head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ hasheadline=1 - nnext=`expr $nsucc + 1` + nnext=$(expr $nsucc + 1) else head -n +$n $i > $i.head.tmp$$ hasheadline=0 @@ -44,9 +41,9 @@ for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o cat $newheader >> $i.tmp$$ tail -n +$nnext $i >> $i.tmp$$ mv $i.tmp$$ $i - modified=`expr $modified + 1` + modified=$(expr $modified + 1) else - kept=`expr $kept + 1` + kept=$(expr $kept + 1) fi rm $i.head.tmp$$ done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index c6687b9731..5f9f326750 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -78,13 +78,38 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'." Note that this function is executed before _Coqproject is read if it exists." (let ((dir (coqdev-default-directory))) (when dir - (unless coq-prog-args - (setq coq-prog-args - `("-coqlib" ,dir - "-topfile" ,buffer-file-name))) - (setq-local coq-prog-name (concat dir "bin/coqtop"))))) + (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) +(defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg" + "Command run by `coqdev-ocamldebug'") + +(defun coqdev-ocamldebug () + "Runs a command in an ocamldebug buffer." + (interactive) + (let* ((dir (read-directory-name "Run from directory: " + (coqdev-default-directory))) + (name "ocamldebug-coq") + (buffer-name (concat "*" name "*"))) + (pop-to-buffer buffer-name) + (unless (comint-check-proc buffer-name) + (setq default-directory dir) + (setq coqdev-ocamldebug-command + (read-from-minibuffer "Command to run: " + coqdev-ocamldebug-command)) + (let* ((cmdlist (tuareg--split-args coqdev-ocamldebug-command)) + (cmdlist (mapcar #'substitute-in-file-name cmdlist))) + (apply #'make-comint name + (car cmdlist) + nil + (cdr cmdlist)) + (set-process-filter (get-buffer-process (current-buffer)) + #'ocamldebug-filter) + (set-process-sentinel (get-buffer-process (current-buffer)) + #'ocamldebug-sentinel) + (ocamldebug-mode))) + (ocamldebug-set-buffer))) + ;; This Elisp snippet adds a regexp parser for the format of Anomaly ;; backtraces (coqc -bt ...), to the error parser of the Compilation ;; mode (C-c C-c: "Compile command: ..."). File locations in traces diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index ff9b32fe78..0338cd42c7 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -73,8 +73,6 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') -BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') -BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v') TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) @@ -401,34 +399,6 @@ dev/tools/update-compat.py --assert-unchanged %s || exit $? ''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip() update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args) -def update_bug_4789(new_versions, **args): - # we always update this compat notation to oldest - # currently-supported compat version, which should never be the - # current version - with open(BUG_4798_PATH, 'r') as f: contents = f.read() - new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "%s"). -Check match 2 with 0 => 0 | S n => n end. (* fails *) -""" % new_versions[0] - update_if_changed(contents, new_contents, BUG_4798_PATH, **args) - -def update_bug_9166(new_versions, **args): - # we always update this compat notation to oldest - # currently-supported compat version, which should never be the - # current version - with open(BUG_9166_PATH, 'r') as f: contents = f.read() - new_contents = BUG_HEADER + r"""Set Warnings "+deprecated". - -Notation bar := option (compat "%s"). - -Definition foo (x: nat) : nat := - match x with - | 0 => 0 - | S bar => bar - end. -""" % new_versions[0] - update_if_changed(contents, new_contents, BUG_9166_PATH, **args) - def update_compat_notations_in(old_versions, new_versions, contents): for v in old_versions: if v not in new_versions: @@ -508,7 +478,5 @@ if __name__ == '__main__': update_test_suite(new_versions, **args) update_test_suite_run(**args) update_doc_index(new_versions, **args) - update_bug_4789(new_versions, **args) - update_bug_9166(new_versions, **args) update_compat_notations(known_versions, new_versions, **args) display_git_grep(known_versions, new_versions) |