nix-archive-1(type directoryentry(name.githubnode(type directoryentry(name workflowsnode(type directoryentry(name coq-tests.ymlnode(typeregularcontents«name: Coq Tests on: push: branches: - main pull_request: branches: - '**' paths: - '.github/workflows/coq-tests.yml' - 'tox.ini' - 'python/coqtop.py' - 'python/xmlInterface.py' - 'tests/coq/**' concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true jobs: coq-tests: name: Coq integration tests # Allow installing Python 3.6 (actions/setup-python#544). runs-on: ubuntu-20.04 # runs-on: ubuntu-latest strategy: matrix: coq_version: - '8.4' - '8.5' - '8.6' - '8.7' - '8.8' - '8.9' - '8.10' - '8.11' - '8.12' - '8.13' - '8.14' - '8.15' - '8.16' - '8.17' - '8.18' - '8.19' - 'master' py_version: ['3.6'] steps: - uses: actions/checkout@v4 - name: Install Nix uses: cachix/install-nix-action@v25 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Install Cachix uses: cachix/cachix-action@v14 with: name: coq skipPush: true - name: Set up Nix cache # Only Coq master needs additional caching. if: ${{ matrix.coq_version == 'master' }} uses: DeterminateSystems/magic-nix-cache-action@v2 - name: Install Coq ${{ matrix.coq_version }} run: nix-env -j auto --cores 0 -i -f ci/coq.nix --argstr version ${{ matrix.coq_version }} - name: Install Python ${{ matrix.py_version }} uses: actions/setup-python@v5 with: python-version: ${{ matrix.py_version }} - name: Install dependencies run: | python -m pip install --upgrade pip pip install tox - name: Run Coq tests run: | coqtop --version python --version tox -e coq-py36 ))entry(namelint.ymlnode(typeregularcontents—name: Lint on: push: branches: - main pull_request: branches: - '**' paths: - '.github/workflows/lint.yml' - 'tox.ini' - 'setup.cfg' - '.pylintrc' - '**.py' concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true jobs: lint: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - name: Set up Python uses: actions/setup-python@v5 with: python-version: '3.10' - name: Install dependencies run: | python -m pip install --upgrade pip pip install tox - name: Run linters run: tox -e check-all ))entry(namepython-tests.ymlnode(typeregularcontentsŸname: Python Tests on: push: branches: - main pull_request: branches: - '**' paths: - '.github/workflows/python-tests.yml' - 'tox.ini' - '**.py' concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true jobs: py-tests: name: Python unit tests # Allow installing Python 3.6 (actions/setup-python#544). runs-on: ubuntu-20.04 # runs-on: ubuntu-latest strategy: matrix: py_version: ['3.6'] steps: - uses: actions/checkout@v4 - name: Install Python ${{ matrix.py_version }} uses: actions/setup-python@v5 with: python-version: ${{ matrix.py_version }} - name: Install dependencies run: | python -m pip install --upgrade pip pip install tox - name: Run Python tests run: | python --version tox -e unit-py36 ))entry(name vim-tests.ymlnode(typeregularcontentsģname: Vim Tests on: push: branches: - main pull_request: branches: - '**' paths: - '.github/workflows/vim-tests.yml' - '**.vim' - 'tests/vim/**' concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true jobs: vim-tests: name: Vim unit tests runs-on: ubuntu-latest strategy: matrix: version: - '7.4' - '8.0' - '8.1' - '8.2' - '9.0' - '9.1' steps: - uses: actions/checkout@v4 - name: Install Nix uses: cachix/install-nix-action@v25 with: nix_path: nixpkgs=channel:nixos-20.09 - name: Install Cachix uses: cachix/cachix-action@v14 with: name: whonore-vim skipPush: true - name: Install Vim ${{ matrix.version }} run: nix-env -j auto --cores 0 -i -f ci/vim.nix --argstr version ${{ matrix.version }} - name: Install Vader uses: actions/checkout@v4 with: repository: junegunn/vader.vim path: ./vader.vim - name: Run Vim tests env: VADER_PATH: $GITHUB_WORKSPACE/vader.vim working-directory: ./tests/vim run: ./run.sh ))))))entry(name .gitignorenode(typeregularcontentse*.py[cod] __pycache__/ doc/tags .cache/ .coverage htmlcov .mypy_cache/ .pytest_cache/ .tox ci/result ))entry(name .pylintrcnode(typeregularcontentsKR[MAIN] # Analyse import fallback blocks. This can be used to support both Python 2 and # 3 compatible code, which means that the block might have code that exists # only in one or another interpreter, leading to false positives when analysed. analyse-fallback-blocks=no # Load and enable all available extensions. Use --list-extensions to see a list # all available extensions. #enable-all-extensions= # In error mode, messages with a category besides ERROR or FATAL are # suppressed, and no reports are done by default. Error mode is compatible with # disabling specific errors. #errors-only= # Always return a 0 (non-error) status code, even if lint errors are found. # This is primarily useful in continuous integration scripts. #exit-zero= # A comma-separated list of package or module names from where C extensions may # be loaded. Extensions are loading into the active Python interpreter and may # run arbitrary code. extension-pkg-allow-list= # A comma-separated list of package or module names from where C extensions may # be loaded. Extensions are loading into the active Python interpreter and may # run arbitrary code. (This is an alternative name to extension-pkg-allow-list # for backward compatibility.) extension-pkg-whitelist= # Return non-zero exit code if any of these messages/categories are detected, # even if score is above --fail-under value. Syntax same as enable. Messages # specified are enabled, while categories only check already-enabled messages. fail-on=C, E, F, I, R, W # Specify a score threshold to be exceeded before program exits with error. fail-under=10 # Interpret the stdin as a python script, whose filename needs to be passed as # the module_or_package argument. #from-stdin= # Files or directories to be skipped. They should be base names, not paths. ignore=CVS # Add files or directories matching the regex patterns to the ignore-list. The # regex matches against paths and can be in Posix or Windows format. ignore-paths= # Files or directories matching the regex patterns are skipped. The regex # matches against base names, not paths. The default value ignores Emacs file # locks ignore-patterns= # List of module names for which member attributes should not be checked # (useful for modules/projects where namespaces are manipulated during runtime # and thus existing member attributes cannot be deduced by static analysis). It # supports qualified module names, as well as Unix pattern matching. ignored-modules= # Python code to execute, usually for sys.path manipulation such as # pygtk.require(). #init-hook= # Use multiple processes to speed up Pylint. Specifying 0 will auto-detect the # number of processors available to use, and will cap the count on Windows to # avoid hangs. jobs=0 # Control the amount of potential inferred values when inferring a single # object. This can help the performance when dealing with large functions or # complex, nested conditions. limit-inference-results=100 # List of plugins (as comma separated values of python module names) to load, # usually to register additional checkers. load-plugins=pylint.extensions.for_any_all, pylint.extensions.redefined_loop_name, pylint.extensions.set_membership, # Pickle collected data for later comparisons. persistent=yes # Minimum Python version to use for version dependent checks. Will default to # the version used to run pylint. py-version=3.6 # Discover python modules and packages in the file system subtree. recursive=yes # When enabled, pylint would attempt to guess common misconfiguration and emit # user-friendly hints instead of false-positive error messages. suggestion-mode=yes # Allow loading of arbitrary C extensions. Extensions are imported into the # active Python interpreter and may run arbitrary code. unsafe-load-any-extension=no # In verbose mode, extra non-checker-related info will be displayed. #verbose= [REPORTS] # Python expression which should return a score less than or equal to 10. You # have access to the variables 'fatal', 'error', 'warning', 'refactor', # 'convention', and 'info' which contain the number of messages in each # category, as well as 'statement' which is the total number of statements # analyzed. This score is used by the global evaluation report (RP0004). evaluation=10.0 - ((float(5 * error + warning + refactor + convention) / statement) * 10) # Template used to display messages. This is a python new-style format string # used to format the message information. See doc for all details. msg-template= # Set the output format. Available formats are text, parseable, colorized, json # and msvs (visual studio). You can also give a reporter class, e.g. # mypackage.mymodule.MyReporterClass. output-format=colorized # Tells whether to display a full report or only the messages. reports=no # Activate the evaluation score. score=no [MESSAGES CONTROL] # Only show warnings with the listed confidence levels. Leave empty to show # all. Valid levels: HIGH, CONTROL_FLOW, INFERENCE, INFERENCE_FAILURE, # UNDEFINED. confidence= # Enable the message, report, category or checker with the given id(s). You can # either give multiple identifier separated by comma (,) or put this option # multiple time (only on the command line, not in the configuration file where # it should appear only once). See also the "--disable" option for examples. enable=all # Disable the message, report, category or checker with the given id(s). You # can either give multiple identifiers separated by comma (,) or put this # option multiple times (only on the command line, not in the configuration # file where it should appear only once). You can also use "--disable=all" to # disable everything first and then re-enable specific checks. For example, if # you want to run only the similarities checker, you can use "--disable=all # --enable=similarities". If you want to run only the classes checker, but have # no Warning level messages displayed, use "--disable=all --enable=classes # --disable=W". disable=blacklisted-name, disallowed-name, file-ignored, fixme, invalid-characters-in-docstring, invalid-name, line-too-long, locally-disabled, suppressed-message, too-few-public-methods, too-many-ancestors, too-many-arguments, too-many-boolean-expressions, too-many-branches, too-many-instance-attributes, too-many-lines, too-many-locals, too-many-nested-blocks, too-many-public-methods, too-many-return-statements, too-many-statements, unsubscriptable-object, use-implicit-booleaness-not-comparison-to-string, use-implicit-booleaness-not-comparison-to-zero, wrong-spelling-in-comment, wrong-spelling-in-docstring, [TYPECHECK] # List of decorators that produce context managers, such as # contextlib.contextmanager. Add to this list to register other decorators that # produce valid context managers. contextmanager-decorators=contextlib.contextmanager # List of members which are set dynamically and missed by pylint inference # system, and so shouldn't trigger E1101 when accessed. Python regular # expressions are accepted. generated-members= # Tells whether to warn about missing members when the owner of the attribute # is inferred to be None. ignore-none=yes # This flag controls whether pylint should warn about no-member and similar # checks whenever an opaque object is returned when inferring. The inference # can return multiple potential results while evaluating a Python object, but # some branches might not be evaluated, which results in partial inference. In # that case, it might be useful to still emit no-member and other checks for # the rest of the inferred objects. ignore-on-opaque-inference=yes # List of symbolic message names to ignore for Mixin members. ignored-checks-for-mixins=no-member, not-async-context-manager, not-context-manager, attribute-defined-outside-init # List of class names for which member attributes should not be checked (useful # for classes with dynamically set attributes). This supports the use of # qualified names. ignored-classes=optparse.Values,thread._local,_thread._local # Show a hint with possible names when a member name was not found. The aspect # of finding the hint is based on edit distance. missing-member-hint=yes # The minimum edit distance a name should have in order to be considered a # similar match for a missing member name. missing-member-hint-distance=1 # The total number of similar names that should be taken in consideration when # showing a hint for a missing member. missing-member-max-choices=1 # Regex pattern to define which classes are considered mixins. mixin-class-rgx=.*[Mm]ixin # List of decorators that change the signature of a decorated function. signature-mutators= [EXCEPTIONS] # Exceptions that will emit a warning when caught. overgeneral-exceptions=builtins.Exception [VARIABLES] # List of additional names supposed to be defined in builtins. Remember that # you should avoid defining new builtins when possible. additional-builtins= # Tells whether unused global variables should be treated as a violation. allow-global-unused-variables=yes # List of names allowed to shadow builtins allowed-redefined-builtins= # List of strings which can identify a callback function by name. A callback # name must start or end with one of those strings. callbacks=cb_, _cb # A regular expression matching the name of dummy variables (i.e. expected to # not be used). dummy-variables-rgx=_+$|(_[a-zA-Z0-9_]*[a-zA-Z0-9]+?$)|dummy|^ignored_|^unused_ # Argument names that match this expression will be ignored. Default to name # with leading underscore. ignored-argument-names=_.*|^ignored_|^unused_ # Tells whether we should check for unused import in __init__ files. init-import=no # List of qualified module names which can have objects that can redefine # builtins. redefining-builtins-modules=six.moves,future.builtins [SIMILARITIES] # Comments are removed from the similarity computation ignore-comments=yes # Docstrings are removed from the similarity computation ignore-docstrings=yes # Imports are removed from the similarity computation ignore-imports=no # Signatures are removed from the similarity computation ignore-signatures=yes # Minimum lines number of a similarity. min-similarity-lines=4 [SPELLING] # Limits count of emitted suggestions for spelling mistakes. max-spelling-suggestions=4 # Spelling dictionary name. Available dictionaries: none. To make it work, # install the 'python-enchant' package. spelling-dict= # List of comma separated words that should be considered directives if they # appear at the beginning of a comment and should not be checked. spelling-ignore-comment-directives=fmt: on,fmt: off,noqa:,noqa,nosec,isort:skip,mypy: # List of comma separated words that should not be checked. spelling-ignore-words= # A path to a file that contains the private dictionary; one word per line. spelling-private-dict-file= # Tells whether to store unknown words to the private dictionary (see the # --spelling-private-dict-file option) instead of raising a message. spelling-store-unknown-words=no [LOGGING] # The type of string formatting that logging methods do. `old` means using % # formatting, `new` is for `{}` formatting. logging-format-style=old # Logging modules to check that the string format arguments are in logging # function parameter format. logging-modules=logging [STRING] # This flag controls whether inconsistent-quotes generates a warning when the # character used as a quote delimiter is used inconsistently within a module. check-quote-consistency=no # This flag controls whether the implicit-str-concat should generate a warning # on implicit string concatenation in sequences defined over several lines. check-str-concat-over-line-jumps=no [REFACTORING] # Maximum number of nested blocks for function / method body max-nested-blocks=5 # Complete name of functions that never returns. When checking for # inconsistent-return-statements if a never returning function is called then # it will be considered as an explicit return statement and no message will be # printed. never-returning-functions=sys.exit [FORMAT] # Expected format of line ending, e.g. empty (any line ending), LF or CRLF. expected-line-ending-format= # Regexp for a line that is allowed to be longer than the limit. ignore-long-lines=^\s*(# )??$ # Number of spaces of indent required inside a hanging or continued line. indent-after-paren=4 # String used as indentation unit. This is usually " " (4 spaces) or "\t" (1 # tab). indent-string=' ' # Maximum number of characters on a single line. max-line-length=80 # Maximum number of lines in a module. max-module-lines=1000 # Allow the body of a class to be on the same line as the declaration if body # contains single statement. single-line-class-stmt=no # Allow the body of an if to be on the same line as the test if there is no # else. single-line-if-stmt=no [DESIGN] # List of regular expressions of class ancestor names to ignore when counting # public methods (see R0903) exclude-too-few-public-methods= # List of qualified class names to ignore when counting class parents (see # R0901) ignored-parents= # Maximum number of arguments for function / method. max-args=5 # Maximum number of attributes for a class (see R0902). max-attributes=7 # Maximum number of boolean expressions in an if statement (see R0916). max-bool-expr=5 # Maximum number of branch for function / method body. max-branches=12 # Maximum number of locals for function / method body. max-locals=15 # Maximum number of parents for a class (see R0901). max-parents=7 # Maximum number of public methods for a class (see R0904). max-public-methods=20 # Maximum number of return / yield for function / method body. max-returns=6 # Maximum number of statements in function / method body. max-statements=50 # Minimum number of public methods for a class (see R0903). min-public-methods=2 [CLASSES] # Warn about protected attribute access inside special methods check-protected-access-in-special-methods=no # List of method names used to declare (i.e. assign) instance attributes. defining-attr-methods=__init__, __new__, setUp, _reset # List of member names, which should be excluded from the protected access # warning. exclude-protected=_asdict, _fields, _replace, _source, _make # List of valid names for the first argument in a class method. valid-classmethod-first-arg=cls # List of valid names for the first argument in a metaclass class method. valid-metaclass-classmethod-first-arg=mcs [BASIC] # Naming style matching correct argument names. argument-naming-style=snake_case # Regular expression matching correct argument names. Overrides argument- # naming-style. If left empty, argument names will be checked with the set # naming style. argument-rgx=(([a-z][a-z0-9_]{2,30})|(_[a-z0-9_]*))$ # Naming style matching correct attribute names. attr-naming-style=snake_case # Regular expression matching correct attribute names. Overrides attr-naming- # style. If left empty, attribute names will be checked with the set naming # style. attr-rgx=(([a-z][a-z0-9_]{2,30})|(_[a-z0-9_]*))$ # Bad variable names which should always be refused, separated by a comma. bad-names=foo, bar, baz, toto, tutu, tata # Bad variable names regexes, separated by a comma. If names match any regex, # they will always be refused bad-names-rgxs= # Naming style matching correct class attribute names. class-attribute-naming-style=any # Regular expression matching correct class attribute names. Overrides class- # attribute-naming-style. If left empty, class attribute names will be checked # with the set naming style. class-attribute-rgx=([A-Za-z_][A-Za-z0-9_]{2,30}|(__.*__))$ # Naming style matching correct class constant names. class-const-naming-style=UPPER_CASE # Regular expression matching correct class constant names. Overrides class- # const-naming-style. If left empty, class constant names will be checked with # the set naming style. #class-const-rgx= # Naming style matching correct class names. class-naming-style=PascalCase # Regular expression matching correct class names. Overrides class-naming- # style. If left empty, class names will be checked with the set naming style. class-rgx=[A-Z_][a-zA-Z0-9]+$ # Naming style matching correct constant names. const-naming-style=UPPER_CASE # Regular expression matching correct constant names. Overrides const-naming- # style. If left empty, constant names will be checked with the set naming # style. const-rgx=(([A-Z_][A-Z0-9_]*)|(__.*__))$ # Minimum line length for functions/classes that require docstrings, shorter # ones are exempt. docstring-min-length=-1 # Naming style matching correct function names. function-naming-style=snake_case # Regular expression matching correct function names. Overrides function- # naming-style. If left empty, function names will be checked with the set # naming style. function-rgx=(([a-z][a-z0-9_]{2,30})|(_[a-z0-9_]*))$ # Good variable names which should always be accepted, separated by a comma. good-names=i, j, k, ex, Run, _ # Good variable names regexes, separated by a comma. If names match any regex, # they will always be accepted good-names-rgxs= # Include a hint for the correct naming format with invalid-name. include-naming-hint=no # Naming style matching correct inline iteration names. inlinevar-naming-style=any # Regular expression matching correct inline iteration names. Overrides # inlinevar-naming-style. If left empty, inline iteration names will be checked # with the set naming style. inlinevar-rgx=[A-Za-z_][A-Za-z0-9_]*$ # Naming style matching correct method names. method-naming-style=snake_case # Regular expression matching correct method names. Overrides method-naming- # style. If left empty, method names will be checked with the set naming style. method-rgx=(([a-z][a-z0-9_]{2,30})|(_[a-z0-9_]*))$ # Naming style matching correct module names. module-naming-style=snake_case # Regular expression matching correct module names. Overrides module-naming- # style. If left empty, module names will be checked with the set naming style. module-rgx=(([a-z_][a-z0-9_]*)|([A-Z][a-zA-Z0-9]+))$ # Colon-delimited sets of names that determine each other's naming style when # the name regexes allow several styles. name-group= # Regular expression which should only match function or class names that do # not require a docstring. no-docstring-rgx=^_ # List of decorators that produce properties, such as abc.abstractproperty. Add # to this list to register other decorators that produce valid properties. # These decorators are taken in consideration only for invalid-name. property-classes=abc.abstractproperty # Regular expression matching correct type variable names. If left empty, type # variable names will be checked with the set naming style. #typevar-rgx= # Naming style matching correct variable names. variable-naming-style=snake_case # Regular expression matching correct variable names. Overrides variable- # naming-style. If left empty, variable names will be checked with the set # naming style. variable-rgx=(([a-z][a-z0-9_]{2,30})|(_[a-z0-9_]*))$ [IMPORTS] # List of modules that can be imported at any level, not just the top level # one. allow-any-import-level=typing_extensions # Allow wildcard imports from modules that define __all__. allow-wildcard-with-all=no # Deprecated modules which should not be used, separated by a comma. deprecated-modules=optparse,tkinter.tix # Output a graph (.gv or any supported image format) of external dependencies # to the given file (report RP0402 must not be disabled). ext-import-graph= # Output a graph (.gv or any supported image format) of all (i.e. internal and # external) dependencies to the given file (report RP0402 must not be # disabled). import-graph= # Output a graph (.gv or any supported image format) of internal dependencies # to the given file (report RP0402 must not be disabled). int-import-graph= # Force import order to recognize a module as part of the standard # compatibility libraries. known-standard-library= # Force import order to recognize a module as part of a third party library. known-third-party=enchant # Couples of modules and preferred modules, separated by a comma. preferred-modules= [MISCELLANEOUS] # List of note tags to take in consideration, separated by a comma. notes=FIXME, XXX, TODO # Regular expression of note tags to take in consideration. notes-rgx= ))entry(name CHANGELOG.mdnode(typeregularcontents 9# Change Log ## Unreleased ([main]) ### Added - `g:coqtail_treat_stderr_as_warning` option to ignore unrecognized warnings on stderr. (PR #338) - Add a hook for more flexible keybindings. (PR #339) ### Fixed - Highlight `Structure` as a synonym for `Record`. (PR #357) - Don't try to decode partial JSON responses, avoiding a potential overflow error in NeoVim for very long responses. (PR #353) - Don't highlight comments inside strings. (PR #352) - Highlight `edestruct` correctly. (PR #346) - Highlight `generalize dependent` correctly. (PR #343) - Parse single and double quotes in `_CoqProject` files in the same way as CoqIDE. (PR #342) - Fix rendering of goals panel when no proof is active in Coq >= 8.16. (PR #337) ## [1.7.1] ### Added - Support for Coq 8.19. (PR #336) - Support for Coq 8.18. (PR #329) - Support for Coq 8.17. (PR #324) ### Fixed - Adjusted the default dark-mode GUI colors for `CoqtailChecked` and `CoqtailSent` to make them more legible. See the [README](README.md#syntax-highlighting-and-indentation) for help overriding these defaults. (PR #325) - Refresh proof-progress highlighting correctly when entering/leaving a buffer that is open in multiple windows. (PR #327) ## [1.7.0] ### Added - A command (`CoqOmitToLine`) to advance to a given line while omitting the body of and admitting all intervening opaque proofs. (PR #321) - Display goal names when `Printing Goal Names` is enabled. (PR #310) - Support for the `Subgoals` XML command (>= 8.16 only). This should speed up displaying the current goal when there are many unfocused/shelved/admitted goals with large proof contexts. (PR #309) ### Fixed - Fall back to using `Add` to set options if a best-effort attempt at using `SetOptions` fails. (PR #318) - Use a no-op command that does not hang with `-noinit`. (PR #313) - Joining comments with `J` while the `j` flag is set in `'formatoptions'` does not delete the second line. (PR #307) - Formatting long comments (e.g., with `gqq`) does not stop after the second line. (PR #307) ## [1.6.4] ### Added - Support for Coq 8.16. (PR #264) - Highlight `Register/Register Inline`. (PR #300) ### Fixed - Set the undo history for the Goal and Info panels on updates. (PR #302) - Incorrect indentation of a line following a comment. (PR #299) - Highlight hypotheses separated by a comma on the first line of the hypotheses block in the Goal panel as `coqIdent`. (PR #294) - Incorrect parsing of bracketed goal selectors (`2:{`) with newlines. (PR #292) ## [1.6.3] ### Added - Support for Elpi syntax highlighting and parsing inside `lp:{{ ... }}` blocks. (PR #278) - `g:coqtail_tagfunc` option to enable/disable Coqtail's default `tagfunc`. (PR #272) - Support for Coq 8.15. (PR #266) ### Fixed - Incorrect highlighting of identifiers containing "exists" or "error". (PR #291) - Highlight more query commands. (PR #291) - Highlight `Typeclasses Opaque/Transparent`. (PR #286) - Strip trailing whitespace from the splash screen to make it less ugly when `list` + `listchars=trail:` is set. (PR #284) - Catch and report long warnings from Coqtop that line wrap (`Warning:\n` instead of `Warning: `) instead of aborting. (PR #274) - Broken highlighting and indentation after `Fail Next Obligation`. (PR #268) - Highlight many more tactics. (PR #269) ## [1.6.2] ### Added - `g:coqtail_update_tagstack` option to update the tagstack on `:CoqGotoDef` (enabled by default). (PR #175) ### Fixed - Avoid clearing the Info buffer when `:CoqToLine` advances 0 sentences. (PR #261) - Suppress spurious `TextYankPost` autocmd while getting text selected in Visual mode. (PR #260) - Avoid manually calling `redraw` in NeoVim. (PR #260) ## [1.6.1] ### Added - Code folding for Sections, Modules, and Theorems. (PR #242) - `g:coqtail_inductive_shift` option to control indentation of Inductive constructor branches. (PR #248) ### Fixed - Highlight `Number Notation` and `Declare Custom Entry`. (PR #243) - Crash with `Implicit Type (x : ...)`. (PR #253) - Universe levels inconsistent with those shown by `coqc`. (PR #253) - Indent the line after `Proof using` correctly. (PR #255) - Crash when output contains unprintable characters. (PR #256) ## [1.6.0] ### Added - `g:coqtail_version_compat` option to re-enable old behaviors after breaking changes. (PR #238) ### Fixed - Change ambiguous default mappings to remove delay. **BREAKING**: The default mappings have changed for for `CoqGotoDef` (`cg` -> `cgd`), `CoqGotoGoalEnd` (`cGG` -> `cgG`), `CoqGotoGoalNextStart` (`g]` -> `]g`), `CoqGotoGoalNextEnd` (`G]` -> `]G`), `CoqGotoGoalPrevStart` (`g[` -> `[g`), and `CoqGotoGoalPrevEnd` (`G[` -> `[G`). Set `g:coqtail_version_compat = ['1.5']` to enable the old mappings, or see the [README](README.md#mappings) for help changing these defaults. (PR #238) ## [1.5.2] ### Added - Preliminary support for Coq 8.15. (PR #209) - Support for Coq 8.14. (PRs #211, #213, #240) ## [1.5.1] ### Fixed - Recognize `.` followed by a tab as a sentence ending. (PR #234) - Don't abort if only warnings are printed to `stderr`. Include Coqtop `stderr` in the error message for `coqtail#start`. (PR #226) ## [1.5.0] ### Added - `g:coqtail_coq_path` defaults to `$COQBIN` if it is set. (PR #219) ### Fixed - Jumping to a definition with `:CoqGotoDef` or `:tag` commands works correctly with identifiers that include `'` (a single quote). (PR #218) - Coqtail chooses which `coq(ide)top(.opt)` to use in a more predictable way. It uses `$PATH` (or `g:coqtail_coq_path` if it is set) to find `coqc` (or `g:coqtail_coq_prog` if it is set) and check its version. It then looks for `coqtop` or `coqidetop` (or `g:coqtail_coq_path`) as appropriate in the same directory as `coqc`, taking possible prefixes (e.g., `coq-prover.`) and extensions (e.g., `.opt`) into account. **BREAKING**: If you have multiple versions of Coq installed Coqtail may choose a different one than before. In particular, executables in the current directory are no longer considered by default. Set `g:coqtail_coq_path` explicitly if you rely on this behavior. (PR #216) ## [1.4.1] ### Added - Spell checking in comments. (PR #215) ### Fixed - Return when Coqtop prints to `stderr` instead of waiting on `stdout` indefinitely. (PR #214) - Use case-sensitive search in indent function. (PR #210) - Use `win_execute` when possible while refreshing highlighting to avoid changing windows, which broke certain plugins. (PR #208) - Highlight `Existing Instances`. (PR #207) - Detect when Coqtop crashes on `:CoqStart` and print the error message instead of hanging. (PR #205) - Work around a NeoVim bug with `py3eval` that caused Coqtail to incorrectly detect a lack of Python 3 support. (PR #204) - Display the "Requires Python 3" warning message even if `shortmess+=F` is set. (PR #204) ## [1.4.0] ### Removed - Support for Python <3.6. See [YouCompleteMe] for help with building Vim with Python 3 support. If you are unable to upgrade to Python 3, use the [python2] branch. Nearly all of the changes to the code are internal cleanup so there should be no observable changes in behavior. Please [open an issue] to report any regressions. See [here](https://github.com/whonore/Coqtail/issues/159) for the full list of changes. (PR #188) ## [1.3.1] ### Added - `:CoqJumpToError` command that moves the cursor to the location of the error reported by Coq, if any. (PR #196) ### Fixed - Use `deletebufline` instead of `:delete` when possible to avoid leaving visual mode while updating the Goal and Info panels. (PR #198) - Correctly ignore `(*` and `*)` inside strings. (PR #193) - Print Coq error messages when checking goals or rewinding. (PR #187) - Highlight `Module Import` and `Module Export`. (PRs #195, #202) - Improve highlighting inside sections and modules. (PR #191) - Correctly highlight `..` in recursive notations. (PR #190) - Highlight attributes and skip them when splitting sentences. (PR #152) - Highlight `admit` and `give_up` tactics. (PR #182) - Match non-ASCII letters in identifier syntax highlighting. (PR #184) - Improve syntax highlighting of binders in definitions, theorems, etc. (PR #185) ## [1.3.0] ### Added - Support for highlighting proof diffs. `g:coqtail_auto_set_proof_diffs` can be used to automatically enable diffs on `:CoqStart`. (PR #169) - Support for Coq 8.13. (PR #181) - Support for Coq installed through Snap by checking for the `coq-prover.` prefix as a fallback when looking for `coqidetop`. (PR #180) - Support for multiple `_CoqProject` files. **BREAKING**: renamed `g:coqtail_project_name` to `g:coqtail_project_names` and `b:coqtail_project_file` to `b:coqtail_project_files`. (PR #141) - Match CoqIDE behavior and set the top-level module name based on the file name with `-topfile` (Coq >=8.10 only). (PR #145) - Improved comment autoformatting. Disable with `g:coqtail_noindent_comment`. (PR #146) - Debugging can be enabled with `:CoqToggleDebug` without calling `:CoqStart`. (PR #148) ### Fixed - Correctly handle highlighting of multibyte characters (for real this time). (PR #177) - Preserve jumplist and alternate file when opening Info and Goal panels. (PR #150) - Don't list Info and Goal panel buffers. (PR #151) - Catch exception in `CoqtailServer` when the connection is reset by the peer. (PR #155) - Remember the cursor position in the jumplist before moving it with `:CoqJumpToEnd`. (PR #173) - Various syntax highlighting improvements including basic support for Ltac2. (PRs #139, #143, #149, #153, #156, #172) ### Removed - Dependency on `distutils` if `shutil.which` is available (Python >=3.3). (PR #161) ## [1.2.0] ### Added - Support for Coq 8.12. (PR #120) - `g:coqtail_noimap`, `g:coqtail_map_prefix`, `g:coqtail_imap_prefix` configuration options to control insert-mode mappings. (PR #122) - Mappings for query commands (`cs`, `ch`, etc) now work on the highlighted range in Visual mode. (PR #131) - Commands and mappings now work when called in the Goal and Info panels. (PR #132) ### Fixed - `g:coqtail_coq_path` is now checked on `:CoqStart` instead of on buffer load. (PR #123) - `:CoqStart` no longer fails when the Coq executable is in the current directory. (PR #123) - Various syntax highlighting/indentation improvements. (PRs #124, #126, #127) - No longer crash when checking Coq version if `coqtop.opt` does not exist. (PR #129) - No longer crash on `:CoqStart` when a buffer has no associated file. (PR #137) - Improved interrupt-handling logic, which should reduce the frequency of the case where pending commands are not cleared and `nomodifiable` is set after every command. (PR #130) ## [1.1.0] ### Added - Support for NeoVim >=0.3. (PR #103) - `b:coqtail_coq_prog`/`g:coqtail_coq_prog` configuration option to override the name of the Coq executable. (PR #119) ### Fixed - Lowered priority of Coqtail-related highlighting (`CoqtailChecked`, `CoqtailSent`, `CoqtailError`) so they don't cover existing highlighting, e.g. from `'hlsearch'`. (PR #104) - Only call `coqtail#stop` on `:quit` if it would close the last visible instance of the buffer. (PR #105) - Coqtail highlighting correctly handles multibyte characters. (PR #109) - All pending sentences waiting to be checked by Coq (`CoqtailSent`) are highlighted instead of just the next one. (PR #109) - `:Coq` and `:CoqGotoDef` do not treat arguments containing `"` as comments by removing `-bar` option. (PR #111) - Respect the `$PATH` order when choosing between `coq(ide)top` and `coq(ide)top.opt`. (PR #114) - No longer crash ("E803: ID not found") after `:split`ting the main Coq window. (PR #118) ## [1.0.0] ### Added - Non-blocking communication with Coq using the `+channel` feature (Vim >=8.0 only). - A synchronous fallback for Vim 7.4. - `CoqInterrupt` command that forwards `SIGINT` to the Coq process. - `CoqRestorePanels` command that re-opens the Goal and Info panels in their original positions. - This changelog. Begin using semantic (more or less) versioning. ### Removed - Dependency on `vim` module in Python code. - Dependency on [vimbufsync]. - `CoqMakeMatch` command. It wasn't well thought out and didn't seem very useful. Please [open an issue] if you'd like it to be re-added. ### Fixed - Commands no longer crash when called while Goal or Info panels are closed. ### Deprecated - Python 2 support. See [YouCompleteMe] for help building Vim with Python 3 support. ## [pre-1.0] ### Added - Interactive Coq interface similar to CoqIDE/Proof General. - Support for Vim >=7.4. - Support for Python 2 and 3. - Support for Coq 8.4-8.11. - Support for simultaneous Coq sessions in different buffers. - Locating and parsing of _CoqProject files. - Coq syntax highlighting. - Coq automatic indentation. - `CoqGotoDef` command for jumping to definitions. - `includeexpr` for following imports during autocompletion. - Support for `:tag` commands (only with `+tagfunc`). - Interoperability with [matchup] and [endwise]. [main]: https://github.com/whonore/Coqtail [python2]: https://github.com/whonore/Coqtail/tree/python2 [1.7.1]: https://github.com/whonore/Coqtail/tree/v1.7.1 [1.7.0]: https://github.com/whonore/Coqtail/tree/v1.7.0 [1.6.4]: https://github.com/whonore/Coqtail/tree/v1.6.4 [1.6.3]: https://github.com/whonore/Coqtail/tree/v1.6.3 [1.6.2]: https://github.com/whonore/Coqtail/tree/v1.6.2 [1.6.1]: https://github.com/whonore/Coqtail/tree/v1.6.1 [1.6.0]: https://github.com/whonore/Coqtail/tree/v1.6.0 [1.5.2]: https://github.com/whonore/Coqtail/tree/v1.5.2 [1.5.1]: https://github.com/whonore/Coqtail/tree/v1.5.1 [1.5.0]: https://github.com/whonore/Coqtail/tree/v1.5.0 [1.4.1]: https://github.com/whonore/Coqtail/tree/v1.4.1 [1.4.0]: https://github.com/whonore/Coqtail/tree/v1.4.0 [1.3.1]: https://github.com/whonore/Coqtail/tree/v1.3.1 [1.3.0]: https://github.com/whonore/Coqtail/tree/v1.3.0 [1.2.0]: https://github.com/whonore/Coqtail/tree/v1.2.0 [1.1.0]: https://github.com/whonore/Coqtail/tree/v1.1.0 [1.0.0]: https://github.com/whonore/Coqtail/tree/v1.0.0 [pre-1.0]: https://github.com/whonore/Coqtail/tree/pre-1.0 [open an issue]: https://github.com/whonore/Coqtail/issues [vimbufsync]: https://github.com/let-def/vimbufsync [matchup]: https://github.com/andymass/vim-matchup [endwise]: https://github.com/tpope/vim-endwise [YouCompleteMe]: https://github.com/ycm-core/YouCompleteMe/wiki/Building-Vim-from-source ))entry(nameLICENSEnode(typeregularcontents(MIT License Copyright (c) 2017 whonore Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ))entry(name README.mdnode(typeregularcontents75# Coqtail [![Code style: black](https://img.shields.io/badge/code%20style-black-000000.svg)](https://github.com/ambv/black) [![Vim Tests](https://github.com/whonore/Coqtail/workflows/Vim%20Tests/badge.svg?branch=main)](https://github.com/whonore/Coqtail/actions?query=workflow%3AVim%20Tests) [![Python Tests](https://github.com/whonore/Coqtail/workflows/Python%20Tests/badge.svg?branch=main)](https://github.com/whonore/Coqtail/actions?query=workflow%3APython%20Tests) [![Coq Tests](https://github.com/whonore/Coqtail/workflows/Coq%20Tests/badge.svg?branch=main)](https://github.com/whonore/Coqtail/actions?query=workflow%3ACoq%20Tests) ## Interactive Coq Proofs in Vim Coqtail enables interactive Coq proof development in Vim similar to [CoqIDE] or [ProofGeneral]. It supports: - [Coq 8.4 - 8.19] - Python >=3.6 (see [here](#python-2-support) for older versions) - Vim >=7.4 and Neovim >=0.3 - Simultaneous Coq sessions in different buffers - Non-blocking communication between Vim and Coq (Vim >=8.0 and NeoVim only) ## Installation As a [vim package]: ```sh mkdir -p ~/.vim/pack/coq/start git clone https://github.com/whonore/Coqtail.git ~/.vim/pack/coq/start/Coqtail vim +helptags\ ~/.vim/pack/coq/start/Coqtail/doc +q ``` Using [pathogen]: ```sh git clone https://github.com/whonore/Coqtail.git ~/.vim/bundle/Coqtail vim +Helptags +q ``` Using [Vundle]: ```sh Plugin 'whonore/Coqtail' (add this line in .vimrc) vim +PluginInstall +qa ``` Using [VimPlug]: ```sh Plug 'whonore/Coqtail' (add this line in .vimrc) vim +PlugInstall +qa ``` ### Requirements - Vim compiled with `+python3` (3.6 or later) or the `pynvim` Python package for Neovim - Vim configuration options `filetype plugin on`, and optionally `filetype indent on` and `syntax on` (e.g. in `.vimrc`) - [Coq 8.4 - 8.19] Newer versions of Coq have not yet been tested, but should still work as long as there are no major changes made to the [XML protocol]. Note that for Coq >=8.9, the `coqidetop` executable must be available, which may require additionally installing CoqIDE depending on the installation method. See [here](#coq-executable) for help with pointing Coqtail to the appropriate location. ## Usage Coqtail provides the following commands (see `:help coqtail` for more details): | Command | Mapping | Description | |---|---|---| | **Starting and Stopping** | | | `CoqStart` | `cc` | Launch Coqtail in the current buffer. | | `CoqStop` | `cq` | Quit Coqtail in the current buffer. | | `CoqInterrupt` | `CTRL-C` | Send SIGINT to Coq. | | **Movement** | | | `{n}CoqNext` | `cj` | Send the next `n` (1 by default) sentences to Coq. | | `{n}CoqUndo` | `ck` | Step back `n` (1 by default) sentences. | | `{n}CoqToLine` | `cl` | Send/rewind all sentences up to line `n` (cursor position by default). `n` can also be `$` to check the entire buffer. | | `{n}CoqOmitToLine` | No default (see [Mappings](#mappings)) | Same as `CoqToLine`, but skip processing of and admit all opaque proofs. Similar to Proof General's [`proof-omit-proofs-option`](https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Omitting-proofs-for-speed). See `:help CoqOmitToLine` for more information. | | `CoqToTop` | `cT` | Rewind to the beginning of the file. | | `CoqJumpToEnd` | `cG` | Move the cursor to the end of the checked region. | | `CoqJumpToError` | `cE` | Move the cursor to the start of the error region. | | `CoqGotoDef[!] ` | `cgd` | Populate the quickfix list with possible locations of the definition of `` and try to jump to the first one. If your Vim supports `'tagfunc'` you can also use `CTRL-]`, `:tag`, and friends. | | **Queries** | | | `Coq ` | | Send arbitrary queries to Coq (e.g. `Check`, `About`, `Print`, etc.). | | `Coq Check ` | `ch` | Show the type of `` (the mapping will use the term under the cursor or the highlighted range in visual mode). | | `Coq About ` | `ca` | Show information about ``. | | `Coq Print ` | `cp` | Show the definition of ``. | | `Coq Locate ` | `cf` | Show where `` is defined. | | `Coq Search ` | `cs` | Show theorems about ``. | | **Panel Management** | | | `CoqRestorePanels` | `cr` | Re-open the Goal and Info panels. | | `{n}CoqGotoGoal` | `cgg` | Scroll the Goal panel to the start of the `n`th goal (defaults to 1). Number of lines shown is controlled by `g:coqtail_goal_lines`. | | `{n}CoqGotoGoal!` | `cgG` | Scroll the Goal panel to the end of the `n`th goal. | | `CoqGotoGoalNext` | `]g` | Scroll the Goal panel to the start of the next goal. | | `CoqGotoGoalNext!` | `]G` | Scroll the Goal panel to the end of the next goal. | | `CoqGotoGoalPrev` | `[g` | Scroll the Goal panel to the start of the previous goal. | | `CoqGotoGoalPrev!` | `[G` | Scroll the Goal panel to the end of the previous goal. | ## Configuration ### Mappings The mappings above are set by default, but you can disable them all and define your own by setting `g:coqtail_nomap = 1` in your `.vimrc`. Some of the commands, such as `CoqNext`, also have insert-mode mappings by default, which can be disabled with `g:coqtail_noimap`. Alternatively, you can keep the defaults but remap specific commands. For example, use `map ci CoqInterrupt` to avoid hijacking `CTRL-C`. If a mapping for a command already exists when Coqtail is loaded, the default mapping for that command won't be defined. The `c` prefix may be inconvenient depending on your `mapleader` setting. In that case you can set a custom prefix with `g:coqtail_map_prefix` (or `g:coqtail_imap_prefix` for just insert-mode mappings). Finally, after defining the standard keybindings, Coqtail will call a vim function named `CoqtailHookDefineMappings` (if one is defined). This makes it easy to add additional mappings without removing the standard mappings, and to add mappings which are only active in Coqtail-managed buffers. One way to use this hook is to make bindings for commands which augment the standard Coqtail bindings instead of replacing them. One concrete example is: ```vim function CoqtailHookDefineMappings() imap CoqNext imap CoqToLine imap CoqUndo nmap CoqNext nmap CoqToLine nmap CoqUndo endfunction ``` Adding that snippet to your `.vimrc` would create new bindings for `CoqNext`, `CoqToLine`, and `CoqUndo`. Those bindings would be active in all Coq buffers, including Coqtail panels, but inactive in other buffers. The standard Coqtail bindings (`cj`, etc) would remain active. ### Coq Executable By default Coqtail uses the first `coq(ide)top(.opt)` found in your `PATH`. Use `b:coqtail_coq_path` (or `g:coqtail_coq_path`) to specify a different directory to search in (these are automatically set if the `$COQBIN` environment variable is set). You can also override the name of the Coq executable to use with `b:coqtail_coq_prog` (or `g:coqtail_coq_prog`). For example, to use the [HoTT library](https://github.com/HoTT/HoTT): ```vim let b:coqtail_coq_path = '/path/to/HoTT' let b:coqtail_coq_prog = 'hoqidetop' ``` ### _CoqProject Coqtail understands and will search for `_CoqProject` files on `:CoqStart`. Additional or different project files can be specified with `g:coqtail_project_files`. For example, to include arguments from both `_CoqProject` and `_CoqProject.local`: ```vim let g:coqtail_project_files = ['_CoqProject', '_CoqProject.local'] ``` ### Syntax Highlighting and Indentation Coqtail also comes with an ftdetect script for Coq, as well as modified versions of Vincent Aravantinos' [syntax] and [indent] scripts for Coq. These scripts are used by default but can be disabled by setting `g:coqtail_nosyntax = 1` and `g:coqtail_noindent = 1` respectively. Formatting of comments can be disabled with `g:coqtail_noindent_comment`. In addition to the Coq syntax, Coqtail defines highlighting groups for the sentences that are currently or have already been checked by Coq (`CoqtailSent` and `CoqtailChecked`), any lines that raised an error (`CoqtailError`), and the beginnings and ends of omitted proofs (`CoqtailOmitted`). By default these are defined as: ```vim if &t_Co > 16 if &background ==# 'dark' hi def CoqtailChecked ctermbg=17 guibg=#113311 hi def CoqtailSent ctermbg=60 guibg=#007630 else hi def CoqtailChecked ctermbg=17 guibg=LightGreen hi def CoqtailSent ctermbg=60 guibg=LimeGreen endif else hi def CoqtailChecked ctermbg=4 guibg=LightGreen hi def CoqtailSent ctermbg=7 guibg=LimeGreen endif hi def link CoqtailError Error hi def link CoqtailOmitted coqProofAdmit ``` To override these defaults simply set your own highlighting (`:help :hi`) before `syntax/coq.vim` is sourced (e.g., in your `.vimrc`). Note, however, that many colorschemes call `syntax clear`, which clears user-defined highlighting, so it is recommended to place your settings in a `ColorScheme` autocommand. For example: ```vim augroup CoqtailHighlight autocmd! autocmd ColorScheme * \ hi def CoqtailChecked ctermbg=236 \| hi def CoqtailSent ctermbg=237 augroup END ``` If you feel distracted by the error highlighting while editing a failed sentence, you can use the sequence `cl` (`:CoqToLine`) while the cursor is inside that sentence. If it isn't, you can use `cE` (`:CoqJumpToError`) to move it to an appropriate position. ### Proof Diffs Since 8.9, Coq can generate [proof diffs] to highlight the differences in the proof context between successive steps. To enable proof diffs manually, use `:Coq Set Diffs "on"` or `:Coq Set Diffs "removed"`. To automatically enable proof diffs on every `:CoqStart`, set `g:coqtail_auto_set_proof_diffs = 'on'` (or `= 'removed'`). By default, Coqtail highlights these diffs as follows: ```vim hi def link CoqtailDiffAdded DiffText hi def link CoqtailDiffAddedBg DiffChange hi def link CoqtailDiffRemoved DiffDelete hi def link CoqtailDiffRemovedBg DiffDelete ``` See the [above instructions](#syntax-highlighting-and-indentation) on how to override these defaults. ### More Options See `:help coqtail-configuration` for a description of all the configuration options. ## Vim Plugin Interoperability ### Jumping between matches Coqtail defines `b:match_words` patterns to support jumping between matched text with `%` using the [matchup] or [matchit] plugins. ### Automatically closing blocks Coqtail defines patterns to enable automatic insertion of the appropriate `End` command for code blocks such as `Section`s, `Module`s, and `match` expressions with [endwise]. ### Tags Coqtail supports the `:tag` family of commands by locating a term on the fly with `tagfunc`. However, as this relies on Coq's `Locate` command, it only works if the point where the term is defined has already been evaluated by Coq. An alternative is to disable Coqtail's default `tagfunc` (`let g:coqtail_tagfunc = 0`) and instead use [universal-ctags] in conjunction with [coq.ctags], to statically generate a `tags` file. This works especially well with something like the [gutentags] plugin to automatically keep the `tags` file in sync with the Coq source. ### Latex/Unicode input Coqtail and Coq can handle non-ASCII characters in identifiers, notations, etc., but Coqtail does not provide a method for inputting these characters itself. Instead one can use one of the native Vim options (e.g., [`i_CTRL-K`](https://vimhelp.org/insert.txt.html#i_CTRL-K) or [`i_CTRL-V_digit`](https://vimhelp.org/insert.txt.html#i_CTRL-V_digit)) or a plugin like [latex-unicoder] or [unicode.vim]. ## Thanks Parts of Coqtail were originally inspired by/adapted from [Coquille] (MIT License, Copyright (c) 2013, Thomas Refis). --- #### Python 2 Support Python 2 and 3.5 have reached their [end-of-life](https://pythonclock.org/) so Coqtail no longer supports them in order to simplify the code and take advantage of newer features. See [YouCompleteMe] for help building Vim with Python 3 support. If you cannot upgrade Vim, the [python2] branch still supports older Pythons. [python2]: https://github.com/whonore/Coqtail/tree/python2 [Coq 8.4 - 8.19]: https://coq.inria.fr/download [CoqIDE]: https://coq.inria.fr/refman/practical-tools/coqide.html [ProofGeneral]: https://proofgeneral.github.io/ [XML protocol]: https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md [vim package]: https://vimhelp.org/repeat.txt.html#packages [pathogen]: https://github.com/tpope/vim-pathogen [Vundle]: https://github.com/VundleVim/Vundle.vim [VimPlug]: https://github.com/junegunn/vim-plug [syntax]: http://www.vim.org/scripts/script.php?script_id=2063 [indent]: http://www.vim.org/scripts/script.php?script_id=2079 [matchup]: https://github.com/andymass/vim-matchup [matchit]: http://ftp.vim.org/pub/vim/runtime/macros/matchit.txt [endwise]: https://github.com/tpope/vim-endwise [proof diffs]: https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Diffs [Coquille]: https://github.com/the-lambda-church/coquille [YouCompleteMe]: https://github.com/ycm-core/YouCompleteMe/wiki/Building-Vim-from-source [universal-ctags]: https://github.com/universal-ctags/ctags [coq.ctags]: https://github.com/tomtomjhj/coq.ctags [gutentags]: https://github.com/ludovicchabant/vim-gutentags [latex-unicoder]: https://github.com/joom/latex-unicoder.vim [unicode.vim]: https://github.com/chrisbra/unicode.vim ))entry(nameautoloadnode(type directoryentry(namecoqtailnode(type directoryentry(name channel.vimnode(typeregularcontentsY" Author: Wolf Honore " Python communication channels. function! coqtail#channel#new() abort let l:chan = {'handle': -1} for l:f in ['open', 'close', 'status', 'sendexpr', 'evalexpr'] let l:chan[l:f] = function('s:' . l:f) endfor return l:chan endfunction if g:coqtail#compat#has_channel && !g:coqtail#compat#nvim function! s:open(address) dict abort let l:chanopts = {'mode': 'json', 'timeout': 5000} let self.handle = ch_open(a:address, l:chanopts) return self.handle endfunction function! s:close() dict abort return ch_close(self.handle) endfunction function! s:status() dict abort return ch_status(self.handle) endfunction function! s:sendexpr(expr, options) dict abort return ch_sendexpr(self.handle, a:expr, a:options) endfunction function! s:evalexpr(expr, options) dict abort return ch_evalexpr(self.handle, a:expr, a:options) endfunction elseif g:coqtail#compat#nvim " Rate in ms to check if Coqtail is done computing. let s:poll_rate = 10 " Unique message ID. let s:msg_id = 0 " Coqtail responses to synchronous messages. let s:replies_raw = [''] let s:replies = {} " Callbacks for asynchronous messages. let s:callbacks = {} function! s:open(address) dict abort let l:chanopts = {'on_data': function('s:chanrecv'), 'data_buffered': 0} let self.handle = sockconnect('tcp', a:address, l:chanopts) return self.handle endfunction function! s:close() dict abort return chanclose(self.handle) endfunction function! s:status() dict abort return nvim_get_chan_info(self.handle) != {} ? 'open' : '' endfunction function! s:pre_send(expr) abort let s:msg_id += 1 return [s:msg_id, [json_encode([s:msg_id, a:expr]), '']] endfunction function! s:sendexpr(expr, options) dict abort let [l:msg_id, l:msg] = s:pre_send(a:expr) let s:callbacks[l:msg_id] = a:options.callback call chansend(self.handle, l:msg) endfunction function! s:evalexpr(expr, options) dict abort let [l:msg_id, l:msg] = s:pre_send(a:expr) let s:replies[l:msg_id] = {} call chansend(self.handle, l:msg) " NOTE: only `'timeout': 0` is used now if get(a:options, 'timeout', -1) == 0 return '' endif while s:replies[l:msg_id] == {} execute printf('sleep %dm', s:poll_rate) endwhile let l:res = s:replies[l:msg_id] unlet s:replies[l:msg_id] return l:res endfunction " Handle replies from Coqtail. function! s:chanrecv(handle, msg, event) abort " Every element of a:msg except the first and last is a complete line and " is expected to be valid JSON. The first and last elements may be partial " lines where the first is a continuation of the previous last element. By " appending the first element of a:msg to the last of s:replies_raw, we " guarantee that every element of s:replies_raw except the last one is a " complete reply. When the last line of the reply is received, " s:replies_raw will be ['']. let s:replies_raw[-1] .= a:msg[0] let s:replies_raw += a:msg[1:] " Parse complete replies (all but the last). for l:reply in s:replies_raw[:-2] let l:res = json_decode(l:reply) if l:res[0] ==# 'call' let [l:func, l:args; l:msg_id] = l:res[1:] let l:val = call(l:func, l:args) " Reply only if expected if len(l:msg_id) == 1 call chansend(a:handle, [json_encode([l:msg_id[0], l:val]), '']) endif else let [l:msg_id, l:data] = l:res " Return or execute callback if has_key(s:replies, l:msg_id) let s:replies[l:msg_id] = l:data elseif has_key(s:callbacks, l:msg_id) call call(s:callbacks[l:msg_id], [a:handle, l:data]) unlet s:callbacks[l:msg_id] endif endif endfor " Remove parsed replies (all but the last). let s:replies_raw = [s:replies_raw[-1]] endfunction else py3 from coqtail import ChannelManager " Rate in ms to check if Coqtail is done computing. let s:poll_rate = 10 " Unique session ID. let s:session = 0 function! s:open(address) dict abort let self.handle = py3eval(printf('ChannelManager.open("%s")', a:address)) return self.handle endfunction function! s:close() dict abort return py3eval(printf('ChannelManager.close(%d)', self.handle)) endfunction function! s:status() dict abort return py3eval(printf('ChannelManager.status(%d)', self.handle)) endfunction function! s:sendexpr(expr, options) dict abort echoerr 'Calling ch_sendexpr in synchronous mode.' endfunction " Send a command to Coqtail and wait for the response. function! s:send_wait(handle, session, expr, reply_id) abort let l:response = a:expr[0] == -1 let l:returns = l:response || a:expr[1] !=# 'interrupt' " In Vim 7.4, json_encode(expand('%')) returns v:null instead of "", " which breaks pyeval if has_key(a:expr[2], 'opts') && a:expr[2].opts.filename ==# '' let a:expr[2].opts.filename = '' endif call py3eval(printf( \ 'ChannelManager.send(%d, %s, %s, reply_id=%s, returns=bool(%s))', \ a:handle, \ l:returns ? a:session : 'None', \ json_encode(l:response ? a:expr[1] : a:expr), \ a:reply_id != 0 ? a:reply_id : 'None', \ l:returns \)) " Continually check if Coqtail is done computing let l:poll = printf('ChannelManager.poll(%d)', a:handle) while l:returns let l:res = json_decode(py3eval(l:poll)) if type(l:res) == g:coqtail#compat#t_list return l:res endif execute printf('sleep %dm', s:poll_rate) endwhile return v:null endfunction " Send a command to execute and reply to any requests from Coqtail. function! s:evalexpr(expr, options) dict abort let s:session += 1 let l:session = s:session let l:res = v:null let l:did_int = 0 " Retry until Coqtop responds while 1 try let l:res = s:send_wait(self.handle, l:session, a:expr, 0) " Handle requests while type(l:res) == g:coqtail#compat#t_list && l:res[0] ==# 'call' let l:val = call(l:res[1], l:res[2]) let l:res = s:send_wait(self.handle, l:session, [-1, l:val, {}], l:res[-1]) endwhile catch /^Vim:Interrupt$/ " Interrupt Coqtop and retry if l:did_int call coqtail#util#err('Coqtail is stuck. Try restarting to fix.') return v:null endif let l:did_int = 1 call s:send_wait(self.handle, l:session, [a:expr[0], 'interrupt', {}], 0) continue endtry return type(l:res) == g:coqtail#compat#t_list ? l:res[1] : v:null endwhile endfunction endif ))entry(name compat.vimnode(typeregularcontents: " Author: Wolf Honore " Python and Vim compatibility definitions. " Vim compatibility. let g:coqtail#compat#t_dict = type({}) let g:coqtail#compat#t_list = type([]) let g:coqtail#compat#t_string = type('') let g:coqtail#compat#nvim = has('nvim') let g:coqtail#compat#has_channel = (has('channel') && has('patch-8.0.0001')) || g:coqtail#compat#nvim let g:coqtail#compat#has_tagstack = exists('*gettagstack') && exists('*settagstack') let g:coqtail#compat#has_tagstack_truncate = has('patch-8.2.0077') " Has a stable version of `win_execute`. " If `return` is true then the function must jump back to original window " before returning. It can be set to false to avoid unnecessary jumps in the " compatibility fallback (e.g., if `win_execute` is called in a loop). let g:coqtail#compat#has_win_execute = has('patch-8.2.0137') || has('nvim-0.5') if g:coqtail#compat#has_win_execute function! s:win_execute(id, cmd, return) abort call win_execute(a:id, a:cmd, '') endfunction else function! s:win_execute(id, cmd, return) abort if a:return let l:cur_winid = win_getid() endif call win_gotoid(a:id) call execute(a:cmd, '') if a:return call win_gotoid(l:cur_winid) endif endfunction endif " Call a function using a compatible version of `win_execute`. Calling " `s:win_execute` directly doesn't work because variables are expanded in the " function rather than at the call site. " E.g., `call s:win_execute(1000, 'call s:f(l:x)', 0)` would fail because `s:f` " and `l:x` don't exist. function! coqtail#compat#win_call(id, func, args, return) abort let l:cmd = printf('call call(%s, %s)', string(a:func), a:args) call s:win_execute(a:id, l:cmd, a:return) endfunction " Use `deletebufline` when available because `:delete` forces vim to exit visual mode. if exists('*deletebufline') function! coqtail#compat#deleteline(first, last) abort silent call deletebufline('%', a:first, a:last) endfunction else function! coqtail#compat#deleteline(first, last) abort execute 'silent' a:first ',' a:last 'delete _' endfunction endif " Replace the entire contents of a buffer. function! coqtail#compat#replacelines(lines) abort call coqtail#compat#deleteline(1, '$') call append(0, a:lines) " this leaves an empty line at the bottom call coqtail#compat#deleteline('$', '$') endfunction function! coqtail#compat#init(python_dir) abort " Workaround for a NeoVim bug where py3eval returns v:null the first time " it's called. " See: https://github.com/neovim/neovim/issues/14438 silent! call py3eval('0') if !(has('python3') && py3eval('sys.version_info[:2] >= (3, 6)')) return 0 endif " Add python directory to path so Python functions can be called. py3 import vim py3 if not vim.eval('a:python_dir') in sys.path: \ sys.path.insert(0, vim.eval('a:python_dir')) return 1 endfunction ))entry(namecoqproject.vimnode(typeregularcontents”" Author: Wolf Honore " Locate and parse _CoqProject files. " Parser adapted from https://github.com/coq/coq/blob/v8.19/lib/coqProject_file.ml. function! s:parse_skip_comment(s) abort let l:s = a:s while !empty(l:s) let l:c = l:s[0] let l:s = l:s[1:] if l:c ==# "\n" break endif endwhile return l:s endfunction function! s:parse_string2(s) abort let l:buf = '' let l:s = a:s while !empty(l:s) let l:c = l:s[0] let l:s = l:s[1:] if l:c ==# '"' break else let l:buf .= l:c endif endwhile return [l:s, l:buf] endfunction function! s:parse_string(s) abort let l:buf = '' let l:s = a:s while !empty(l:s) let l:c = l:s[0] let l:s = l:s[1:] if l:c ==# ' ' || l:c ==# "\r" || l:c ==# "\n" || l:c ==# "\t" break elseif l:c ==# '#' let l:s = s:parse_skip_comment(l:s) else let l:buf .= l:c endif endwhile return [l:s, l:buf] endfunction function! s:parse_args(s) abort let l:accu = [] let l:s = a:s while !empty(l:s) let l:c = l:s[0] let l:s = l:s[1:] if l:c ==# ' ' || l:c ==# "\r" || l:c ==# "\n" || l:c ==# "\t" elseif l:c ==# '#' let l:s = s:parse_skip_comment(l:s) elseif l:c ==# '"' let [l:s, l:str] = s:parse_string2(l:s) let l:accu = add(l:accu, l:str) else let [l:s, l:str] = s:parse_string(l:s) let l:accu = add(l:accu, l:c . l:str) endif endwhile return l:accu endfunction function! s:process_extra_args(arg) abort let l:out_list = [] let l:arg = a:arg let l:inside_quotes = 0 let l:has_leftovers = 0 let l:buf = '' while !empty(l:arg) let l:c = l:arg[0] let l:arg = l:arg[1:] if l:c ==# "'" let l:inside_quotes = !l:inside_quotes let l:has_leftovers = 1 elseif l:c ==# ' ' if l:inside_quotes let l:has_leftovers = 1 let l:buf .= ' ' elseif l:has_leftovers let l:has_leftovers = 0 let l:out_list = add(l:out_list, l:buf) let l:buf = '' endif else let l:has_leftovers = 1 let l:buf .= l:c endif endwhile if l:has_leftovers let l:out_list = add(l:out_list, l:buf) endif return l:out_list endfunction " Parse a _CoqProject file into options that can be passed to Coqtop. function! coqtail#coqproject#parse(file) abort let l:dir = fnamemodify(a:file, ':p:h') let l:dir_opts = {'-R': 2, '-Q': 2, '-I': 1, '-include': 1} let l:txt = join(readfile(a:file), "\n") let l:raw_args = s:parse_args(l:txt) let l:proj_args = [] let l:idx = 0 while l:idx < len(l:raw_args) " Make paths absolute for -R, -Q, etc if has_key(l:dir_opts, l:raw_args[l:idx]) let l:absdir = l:raw_args[l:idx + 1] if l:absdir[0] !=# '/' " Join relative paths with 'l:dir' let l:absdir = join([l:dir, l:absdir], '/') endif let l:raw_args[l:idx + 1] = fnamemodify(l:absdir, ':p') " Can be '-R dir -as coqdir' in 8.4 let l:end = l:idx + l:dir_opts[l:raw_args[l:idx]] if l:raw_args[l:end] ==# '-as' || get(l:raw_args, l:end + 1, '') ==# '-as' let l:end = l:idx + 3 endif let l:proj_args += l:raw_args[l:idx : l:end] let l:idx = l:end endif " Pass through options following -arg if l:raw_args[l:idx] ==# '-arg' let l:proj_args += s:process_extra_args(l:raw_args[l:idx + 1]) let l:idx += 1 endif let l:idx += 1 endwhile return l:proj_args endfunction " Find Coq project files in 'g:coqtail_project_names' searching upwards from " the current directory. Return the file names and a list of arguments to pass " to Coqtop. function! coqtail#coqproject#locate() abort let l:files = [] let l:args = [] for l:proj in g:coqtail_project_names let l:file = findfile(l:proj, '.;') if l:file !=# '' let l:files = add(l:files, l:file) let l:args += coqtail#coqproject#parse(l:file) endif endfor return [l:files, l:args] endfunction ))entry(name panels.vimnode(typeregularcontentsē-" Author: Wolf Honore " Goal and Info panel management. " Unique suffix for auxiliary panel names. let s:counter = 0 " Panel identifiers. let g:coqtail#panels#none = '' let g:coqtail#panels#main = 'main' let g:coqtail#panels#goal = 'goal' let g:coqtail#panels#info = 'info' let g:coqtail#panels#aux = [g:coqtail#panels#goal, g:coqtail#panels#info] " Highlighting groups. let s:hlgroups = [ \ ['checked', 'CoqtailChecked'], \ ['sent', 'CoqtailSent'], \ ['error', 'CoqtailError'], \ ['omitted', 'CoqtailOmitted'] \] let s:richpp_hlgroups = { \ 'diff.added': 'CoqtailDiffAdded', \ 'diff.removed': 'CoqtailDiffRemoved', \ 'diff.added.bg': 'CoqtailDiffAddedBg', \ 'diff.removed.bg': 'CoqtailDiffRemovedBg' \} " Default panel layout. if !exists('g:coqtail_panel_layout') let g:coqtail_panel_layout = { \ g:coqtail#panels#goal: \ [[g:coqtail#panels#info, 'above'], [g:coqtail#panels#main, 'right']], \ g:coqtail#panels#info: \ [[g:coqtail#panels#goal, 'below'], [g:coqtail#panels#main, 'right']] \} endif " Default panel scroll options. if !exists('g:coqtail_panel_scroll') let g:coqtail_panel_scroll = { \ g:coqtail#panels#goal: 0, \ g:coqtail#panels#info: 1 \} endif " Return the panels dictionary for buf. function! s:panels(buf) abort return getbufvar(a:buf, 'coqtail_panel_bufs', {}) endfunction " Open and initialize goal/info panel. function! s:init(name) abort let l:name = a:name . 's' let l:bufname = substitute(a:name, '\l', '\u\0', '') " badd forces a new buffer to be created in case the main buffer is empty execute 'keepjumps badd ' . l:bufname . s:counter execute 'silent keepjumps keepalt hide edit ' . l:bufname . s:counter setlocal buftype=nofile execute 'setlocal filetype=coq-' . l:name setlocal noswapfile setlocal bufhidden=hide setlocal nobuflisted setlocal nocursorline setlocal wrap setlocal undolevels=50 let b:coqtail_panel_open = 1 let b:coqtail_panel_size = [-1, -1] let b:coqtail_panel_richpp = [] return bufnr('%') endfunction " Create buffers for the auxiliary panels. function! coqtail#panels#init() abort let l:main_buf = bufnr('%') let l:curpos = getcurpos()[1:] let l:coqtail_panel_bufs = {g:coqtail#panels#main: l:main_buf} " Show saved highlights when the buffer is newly displayed in a window. augroup coqtail#RecallHighlights autocmd! * autocmd BufEnter \ if !exists('w:coqtail_highlights') && exists('b:coqtail_highlights') \| call s:updatehl(bufnr('%'), b:coqtail_highlights) \|endif augroup END " Add panels for l:panel in g:coqtail#panels#aux let l:coqtail_panel_bufs[l:panel] = s:init(l:panel) endfor for l:buf in values(l:coqtail_panel_bufs) call setbufvar(l:buf, 'coqtail_panel_bufs', l:coqtail_panel_bufs) endfor " Switch back to main panel execute 'silent keepjumps keepalt buffer ' . l:main_buf call cursor(l:curpos) let s:counter += 1 endfunction " Detect what panel is focused. function! s:getcurpanel(buf) abort for [l:panel, l:buf] in items(s:panels(a:buf)) if l:buf == a:buf return l:panel endif endfor return g:coqtail#panels#none endfunction " Return the window ID of a panel. function! s:panel_winid(buf, panel) abort return bufwinid(get(s:panels(a:buf), a:panel, -1)) endfunction " Attempt to call a function in the context of a panel. function! s:panel_call(buf, panel, func, args, return) abort let l:winid = s:panel_winid(a:buf, a:panel) if l:winid != -1 call coqtail#compat#win_call(l:winid, a:func, a:args, a:return) endif endfunction " Attempt to switch to a panel from a buffer. function! s:switch_from(buf, panel) abort let l:cur_panel = s:getcurpanel(a:buf) if a:panel != l:cur_panel && a:panel != g:coqtail#panels#none if !win_gotoid(s:panel_winid(a:buf, a:panel)) return g:coqtail#panels#none endif endif return l:cur_panel endfunction " Attempt to switch to a panel from the current buffer. function! coqtail#panels#switch(panel) abort return s:switch_from(bufnr('%'), a:panel) endfunction " Open an auxiliary panel. function! s:open(panel, force) abort let l:from = s:getcurpanel(bufnr('%')) if l:from == g:coqtail#panels#none return 0 endif " Re-open only if not already open, it was open before, or 'force' is true let l:opened = 0 let l:buf = b:coqtail_panel_bufs[a:panel] if bufwinid(l:buf) == -1 && (a:force || getbufvar(l:buf, 'coqtail_panel_open')) " Arrange relative to the first open panel for [l:relative, l:dir] in g:coqtail_panel_layout[a:panel] if coqtail#panels#switch(l:relative) != g:coqtail#panels#none let l:dir = l:dir ==# 'above' ? 'leftabove' \ : l:dir ==# 'below' ? 'rightbelow' \ : l:dir ==# 'left' ? 'vertical leftabove' \ : l:dir ==# 'right' ? 'vertical rightbelow' : '' if l:dir !=# '' execute printf('silent keepjumps keepalt %s sbuffer %d', l:dir, l:buf) clearjumps let b:coqtail_panel_open = 1 let l:opened = l:buf break endif endif endfor endif call coqtail#define_commands() call coqtail#define_mappings() call coqtail#panels#switch(l:from) return l:opened endfunction " Open auxiliary panels. function! coqtail#panels#open(force) abort " Open let l:opened = [] for l:panel in g:coqtail#panels#aux if s:open(l:panel, a:force) let l:opened = add(l:opened, l:panel) endif endfor " Resize for l:panel in l:opened let l:buf = b:coqtail_panel_bufs[l:panel] let l:winnr = bufwinnr(l:buf) let l:size = getbufvar(l:buf, 'coqtail_panel_size') if l:size != [-1, -1] execute printf('vertical %dresize %d', l:winnr, l:size[0]) execute printf('%dresize %d', l:winnr, l:size[1]) endif endfor endfunction " Scroll a panel up so text doesn't go off the top of the screen. function! s:scroll() abort " Check if scrolling is necessary let l:winh = winheight(0) let l:disph = line('w$') - line('w0') + 1 " Scroll if line('w0') != 1 && l:disph < l:winh normal! Gz- endif endfunction " Clear Coqtop highlighting of the current window function! s:clearhl() abort if !exists('w:coqtail_highlights') return endif for [l:var, l:_] in s:hlgroups let l:matches = get(w:coqtail_highlights, l:var, []) for l:match in l:matches call matchdelete(l:match) endfor endfor unlet! w:coqtail_highlights endfunction function! coqtail#panels#cleanuphl() abort if exists('w:coqtail_highlights') && w:coqtail_highlights['buf'] != bufnr('%') call s:clearhl() endif endfunction " Update highlighting of the current window. function! s:updatehl(buf, highlights) abort call s:clearhl() let w:coqtail_highlights = {'buf': a:buf} for [l:var, l:grp] in s:hlgroups let l:hl = a:highlights[l:var] if type(l:hl) == g:coqtail#compat#t_string let w:coqtail_highlights[l:var] = [matchadd(l:grp, l:hl, -10)] elseif type(l:hl) == g:coqtail#compat#t_list " NOTE: add positions one at a time to work around 8-position maximum in " older Vims. let l:matches = [] for l:pos in l:hl let l:matches = add(l:matches, matchaddpos(l:grp, [l:pos], -10)) endfor let w:coqtail_highlights[l:var] = l:matches endif endfor endfunction " Close auxiliary panels and clear highlighting. function! coqtail#panels#hide() abort if coqtail#panels#switch(g:coqtail#panels#main) == g:coqtail#panels#none return endif call s:clearhl() " Hide other panels let l:toclose = [] for l:panel in g:coqtail#panels#aux let l:buf = b:coqtail_panel_bufs[l:panel] let l:winid = bufwinid(l:buf) call setbufvar(l:buf, 'coqtail_panel_open', l:winid != -1) call setbufvar(l:buf, 'coqtail_panel_size', [winwidth(l:winid), winheight(l:winid)]) call setbufvar(l:buf, 'coqtail_panel_richpp', []) if l:winid != -1 let l:toclose = add(l:toclose, l:buf) endif endfor for l:buf in l:toclose execute bufwinnr(l:buf) . 'close!' endfor endfunction " Replace the contents of 'panel' with 'txt'. " This function must be called in the context of the panel's window. function! s:replace(panel, txt, richpp, scroll) abort " Save the view let l:view = winsaveview() " Remove previous highlights for l:match in b:coqtail_panel_richpp call matchdelete(l:match) endfor " Update buffer text let l:old = getline(1, '$') " returns [''] for empty buffer let l:old = l:old ==# [''] ? [] : l:old if l:old !=# a:txt let &l:undolevels = &l:undolevels " explicitly break undo sequence (:h undo-break) call coqtail#compat#replacelines(a:txt) endif " Set new highlights let l:matches = [] for [l:line_no, l:start_pos, l:span, l:hlgroup] in a:richpp if has_key(s:richpp_hlgroups, l:hlgroup) let l:match = matchaddpos( \ s:richpp_hlgroups[l:hlgroup], \ [[l:line_no, l:start_pos, l:span]], \ -10) let l:matches = add(l:matches, l:match) endif endfor let b:coqtail_panel_richpp = l:matches " Restore the view if !a:scroll || !g:coqtail_panel_scroll[a:panel] call winrestview(l:view) endif call s:scroll() endfunction " Refresh the highlighting and auxiliary panels. function! coqtail#panels#refresh(buf, highlights, panels, scroll) abort " Catch interrupt instead of aborting try let l:winids = win_findbuf(a:buf) let l:refreshing = getbufvar(a:buf, 'coqtail_refreshing', 0) if l:winids == [] || l:refreshing return endif call setbufvar(a:buf, 'coqtail_refreshing', 1) let l:cur_winid = win_getid() " Update highlighting call setbufvar(a:buf, 'coqtail_highlights', a:highlights) for l:winid in l:winids call coqtail#compat#win_call( \ l:winid, \ function('s:updatehl'), \ [a:buf, a:highlights], \ 0) endfor " Update panels for [l:panel, l:panel_data] in items(a:panels) let [l:txt, l:richpp] = l:panel_data call s:panel_call( \ a:buf, \ l:panel, \ function('s:replace'), \ [l:panel, l:txt, l:richpp, a:scroll], \ 0) endfor catch /^Vim:Interrupt$/ finally if !g:coqtail#compat#has_win_execute " l:cur_winid might not exist yet silent! call win_gotoid(l:cur_winid) endif call setbufvar(a:buf, 'coqtail_refreshing', 0) " NOTE: NeoVim seems to update often enough on its own to make calling " `redraw` unnecessary, but skipping it in Vim results in noticeable delays " while updating highlighting and text in auxiliary panels delays. " See https://github.com/whonore/Coqtail/pull/260. if !g:coqtail#compat#nvim redraw endif endtry endfunction " Delete panel variables and clear highlighting. function! coqtail#panels#cleanup() abort for l:panel in g:coqtail#panels#aux silent! execute 'bwipeout' b:coqtail_panel_bufs[l:panel] endfor silent! unlet b:coqtail_panel_bufs silent! unlet b:coqtail_highlights let l:cur_winid = win_getid() try for l:winid in win_findbuf(bufnr('%')) call coqtail#compat#win_call( \ l:winid, \ function('s:clearhl'), \ [], \ 0) endfor catch /^Vim:Interrupt$/ finally if !g:coqtail#compat#has_win_execute call win_gotoid(l:cur_winid) endif endtry endfunction " Getter for variables local to the main buffer function! coqtail#panels#getvar(var) abort return getbufvar(b:coqtail_panel_bufs.main, a:var) endfunction " Setter for variables local to the main buffer function! coqtail#panels#setvar(var, val) abort return setbufvar(b:coqtail_panel_bufs.main, a:var, a:val) endfunction ))entry(nameutil.vimnode(typeregularcontents_" Author: Wolf Honore " Utility functions. " Print a message with the specified highlighting. " NOTE: Without 'unsilent' messages triggered during autocmds don't display in " NeoVim because 'shortmess+=F' is set by default. " See: https://github.com/neovim/neovim/issues/8675 function! s:echom(msg, hl) abort execute 'echohl' a:hl for l:line in split(a:msg, '\n') unsilent echom l:line endfor echohl None endfunction " Print a message with warning highlighting. function! coqtail#util#warn(msg) abort call s:echom(a:msg, 'WarningMsg') endfunction " Print a message with error highlighting. function! coqtail#util#err(msg) abort call s:echom(a:msg, 'ErrorMsg') endfunction " Get the word under the cursor using the special '' variable. First " add some characters to the 'iskeyword' option to treat them as part of the " current word. function! coqtail#util#getcurword() abort " Add '.' to definition of a keyword let l:old_keywd = &iskeyword setlocal iskeyword+=. let l:cword = expand('') " Strip trailing '.'s let l:dotidx = match(l:cword, '[.]\+$') if l:dotidx > -1 let l:cword = l:cword[: l:dotidx - 1] endif " Reset iskeyword let &l:iskeyword = l:old_keywd return l:cword endfunction " Get the text selected in Visual mode. function! coqtail#util#getvisual() abort try let l:v_old = @v noautocmd normal! gv"vy return join(split(@v, '\n'), ' ') finally " Restore register let @v = l:v_old endtry endfunction " Remove entries in the quickfix list with the same position. function! s:dedup_qflist() abort let l:qfl = getqflist() let l:seen = {} let l:uniq = [] for l:entry in l:qfl let l:pos = string([l:entry.lnum, l:entry.col]) if !has_key(l:seen, l:pos) let l:seen[l:pos] = 1 let l:uniq = add(l:uniq, l:entry) endif endfor call setqflist(l:uniq) endfunction " Find the positions of all matches. function! s:searchall(text, search) abort let l:matches = [] let l:cnt = 1 while 1 let l:match = matchstrpos(a:text, a:search, 0, l:cnt)[0:2] if l:match[1] == -1 break endif let l:matches = add(l:matches, l:match) let l:cnt += 1 endwhile return l:matches endfunction " Perform a sequence of searches and put the results in the quickfix list. function! coqtail#util#qflist_search(buf, path, searches) abort " Temporarily set the global value of 'iskeyword' to the local value (which " should be Coq's). Otherwise ' is not handled properly by vimgrep. let l:isk = &g:iskeyword let &g:iskeyword = &l:iskeyword let l:found_match = 0 let l:has_file = a:path !=# '' if !l:has_file let l:text = getbufline(a:buf, 1, '$') let l:matches = [] endif for l:search in a:searches let l:search = '\v\C' . l:search try if !l:has_file let l:matches += map( \ s:searchall(l:text, l:search), \ '{"bufnr": a:buf, "text": v:val[0], "lnum": v:val[1] + 1, "col": v:val[2] + 1}') elseif !l:found_match execute 'vimgrep /' . l:search . '/j ' . a:path let l:found_match = 1 else execute 'vimgrepadd /' . l:search . '/j ' . a:path endif catch /^Vim\%((\a\+)\)\=:E480/ endtry endfor if !l:has_file let l:found_match = l:matches != [] if l:found_match call setqflist(l:matches) endif endif if l:found_match " Filter duplicate matches call s:dedup_qflist() endif let &g:iskeyword = l:isk return l:found_match endfunction " Get 'var' from the first scope in 'scopes' in which it is defined. function! coqtail#util#getvar(scopes, var, default) abort return a:scopes != [] \ ? get(a:scopes[0], a:var, coqtail#util#getvar(a:scopes[1:], a:var, a:default)) \ : a:default endfunction " Create a tagstack item to push if the jump is successful. function! coqtail#util#preparetagstack() abort if g:coqtail#compat#has_tagstack && g:coqtail_update_tagstack " Grab the old location (to jump back to) and the word under the cursor " (as a label for the tagstack) let l:pos = [bufnr('%')] + getcurpos()[1:] let l:tag = expand('') return {'bufnr': l:pos[0], 'from': l:pos, 'tagname': l:tag} else return v:null endif endfunction " Push an item to the tagstack. function! coqtail#util#pushtagstack(item) abort if g:coqtail#compat#has_tagstack && g:coqtail_update_tagstack let l:winid = win_getid() let l:tagstack = gettagstack(l:winid) " If the current tagstack index is somewhere in the middle of the stack, we " first truncate everything up to the end, to replicate native behavior of " CTRL-]. This is handled by the 't' action in versions that support it. if g:coqtail#compat#has_tagstack_truncate let l:action = 't' let l:items = [a:item] else let l:action = 'r' let l:items = l:tagstack.items if l:tagstack.curidx <= l:tagstack.length " curidx is always at least 1 unlet l:items[l:tagstack.curidx - 1:] endif call add(l:items, a:item) endif let l:tagstack.items = l:items let l:tagstack.curidx += 1 call settagstack(l:winid, l:tagstack, l:action) endif endfunction ))entry(name version.vimnode(typeregularcontentsƒ" Author: Wolf Honore " Parse and compare version strings. " Pad xs with x on the right up to length n. function! s:rpad(xs, x, n) abort return a:xs + repeat([a:x], a:n - len(a:xs)) endfunction " Split a version into components. " Version is of the form: \d+.\d+((.|pl)\d+|+(alpha|beta|rc)\d+)? function! s:parse(version) abort return s:rpad(split(substitute(a:version, '+.*', '', ''), '\v(\.|pl)'), '0', 3) endfunction " Create a list of pairs. function! s:zip(xs, ys) abort return map(copy(a:xs), '[v:val, a:ys[v:key]]') endfunction " Check if version matches pattern. function! coqtail#version#match(version, pattern) abort for [l:ver, l:pat] in s:zip(s:parse(a:version), s:parse(a:pattern)) if !(l:pat ==# '*' || l:pat ==# l:ver) return 0 endif endfor return 1 endfunction " Check if version is at least pattern. function! coqtail#version#atleast(version, pattern) abort for [l:ver, l:pat] in s:zip(s:parse(a:version), s:parse(a:pattern)) if l:pat ==# '*' || l:pat ==# l:ver continue elseif str2nr(l:pat) < str2nr(l:ver) return 1 else return 0 endif endfor return 1 endfunction ))))entry(name coqtail.vimnode(typeregularcontents®S" Author: Wolf Honore " Coqtail Python interface and window management. " Only source once. if exists('g:loaded_coqtail') finish endif let g:loaded_coqtail = 1 let s:python_dir = expand(':p:h:h') . '/python' let g:coqtail#supported = coqtail#compat#init(s:python_dir) if !g:coqtail#supported call coqtail#util#warn( \ "Coqtail requires Python 3.6 or later.\n" . \ 'See https://github.com/whonore/Coqtail/blob/main/README.md#python-2-support.' \) finish endif py3 from coqtail import CoqtailServer " Initialize global variables. " Default number of lines of a goal to show. let s:goal_lines = 5 " Warning/error messages. let s:unsupported_msg = \ "Coqtail does not officially support your version of Coq (%s).\n" . \ 'Continuing with the interface for the latest supported version (%s).' " Server port. let s:port = -1 " Default CoqProject file name. if !exists('g:coqtail_project_names') let g:coqtail_project_names = ['_CoqProject'] endif " Default to updating the tagstack on coqtail#gotodef. if !exists('g:coqtail_update_tagstack') let g:coqtail_update_tagstack = 1 endif " Default to not treating all stderr messages as warnings. if !exists('g:coqtail_treat_stderr_as_warning') let g:coqtail_treat_stderr_as_warning = 0 endif " Find the path corresponding to 'lib'. Used by includeexpr. function! coqtail#findlib(lib) abort let [l:ok, l:lib] = s:call('find_lib', 'sync', 0, {'lib': a:lib}) return (l:ok && l:lib != v:null) ? l:lib : a:lib endfunction " Find the start of the nth goal. function! s:goal_start(ngoal) abort return search('\m^=\+ (' . a:ngoal . ' /', 'nw') endfunction " Find the end of the nth goal. function! s:goal_end(ngoal) abort if s:goal_start(a:ngoal) == 0 return 0 endif let l:end = s:goal_start(a:ngoal + 1) return l:end != 0 ? l:end - 2 : line('$') endfunction " Determine the next goal's index. function! s:goal_next() abort let l:goal = search('\m^=\+ (\d', 'nWbc') if l:goal == 0 return 1 else return matchstr(getline(l:goal), '\d\+') + 1 endif endfunction " Determine the previous goal's index. function! s:goal_prev() abort let l:next = s:goal_next() return l:next != 1 ? l:next - 2 : 0 endfunction " Place either the start or end of the nth goal at the bottom of the window. function! coqtail#gotogoal(ngoal, start) abort let l:panel = coqtail#panels#switch(g:coqtail#panels#goal) if l:panel == g:coqtail#panels#none " Failed to switch to goal panel return 0 endif " ngoal = -1: next goal, ngoal = -2: previous goal let l:ngoal = \ a:ngoal == -1 ? s:goal_next() : a:ngoal == -2 ? s:goal_prev() : a:ngoal let l:sline = s:goal_start(l:ngoal) let l:eline = s:goal_end(l:ngoal) let l:line = a:start ? l:sline : l:eline if l:line != 0 if a:start let l:off = 1 + get(g:, 'coqtail_goal_lines', s:goal_lines) let l:line = min([l:line + l:off, l:eline]) endif execute 'normal! ' . l:line . 'zb' endif call coqtail#panels#switch(l:panel) return 1 endfunction " Get a list of possible locations of the definition of 'target'. function! s:finddef(target) abort let [l:ok, l:loc] = s:call('find_def', 'sync', 0, {'target': a:target}) return (!l:ok || type(l:loc) != g:coqtail#compat#t_list) ? v:null : l:loc endfunction " Populate the quickfix list with possible locations of the definition of " 'target'. function! coqtail#gotodef(target, bang) abort let l:bang = a:bang ? '!' : '' let l:loc = s:finddef(a:target) if type(l:loc) != g:coqtail#compat#t_list call coqtail#util#warn('Cannot locate ' . a:target . '.') return endif let [l:path, l:searches] = l:loc " Try progressively broader searches if coqtail#util#qflist_search(b:coqtail_panel_bufs.main, l:path, l:searches) " Set usetab instead of opening a new buffer let l:swb = &switchbuf set switchbuf+=usetab let l:item = coqtail#util#preparetagstack() " Jump to first if possible, otherwise open list try execute 'cfirst' . l:bang call coqtail#util#pushtagstack(l:item) catch /^Vim(cfirst):/ botright cwindow endtry " Reset switchbuf let &switchbuf = l:swb endif endfunction " Create a list of tags for 'target'. function! coqtail#gettags(target, flags, info) abort let l:loc = s:finddef(a:target) if type(l:loc) != g:coqtail#compat#t_list return v:null endif let [l:path, l:searches] = l:loc let l:tags = [] for l:search in l:searches let l:tag = {'name': a:target, 'filename': l:path, 'cmd': '/\v' . l:search} let l:tags = add(l:tags, l:tag) endfor return l:tags endfunction " List query options for use in Coq command completion. let s:queries = [ \ 'Search', \ 'SearchAbout', \ 'SearchPattern', \ 'SearchRewrite', \ 'SearchHead', \ 'Check', \ 'Print', \ 'About', \ 'Locate', \ 'Show' \] function! s:querycomplete(arg, cmd, cursor) abort " Only complete one command return len(split(a:cmd)) <= 2 ? join(s:queries, "\n") : '' endfunction " Clean up commands, panels, and autocommands. function! s:cleanup() abort " Switch back to main buffer for cleanup call coqtail#panels#switch(g:coqtail#panels#main) " Clean up autocmds silent! autocmd! coqtail#Quit * silent! autocmd! coqtail#Sync * " Close the channel silent! call b:coqtail_chan.close() let b:coqtail_chan = 0 let b:coqtail_started = 0 " Clean up auxiliary panels call coqtail#panels#cleanup() endfunction " Check if the channel with Coqtail is open. function! s:initted() abort try return coqtail#panels#getvar('coqtail_chan').status() ==# 'open' catch return 0 endtry endfunction " Check if Coqtop has been started. function! s:running() abort try return s:initted() && coqtail#panels#getvar('coqtail_started') catch return 0 endtry endfunction " Send a request to Coqtail. " `cb` is either 'sync', '', or the name of a `:h channel-callback` with " msg: string | {'buf': bufnr, 'ret': any}. " Returns [ok, msg]. function! s:call(cmd, cb, nocoq, args) abort if !((a:nocoq && s:initted()) || (!a:nocoq && s:running())) return [0, -1] endif let a:args.opts = { \ 'encoding': &encoding, \ 'timeout': coqtail#panels#getvar('coqtail_timeout'), \ 'filename': expand('#' . b:coqtail_panel_bufs.main . ':p'), \ 'stderr_is_warning': g:coqtail_treat_stderr_as_warning \} let l:args = [b:coqtail_panel_bufs.main, a:cmd, a:args] if a:cb !=# 'sync' && g:coqtail#compat#has_channel " Async " Increment cmds_pending let l:cmds_pending = coqtail#panels#getvar('coqtail_cmds_pending') call coqtail#panels#setvar('coqtail_cmds_pending', l:cmds_pending + 1) call coqtail#panels#setvar('&modifiable', 0) let l:opts = a:cb !=# '' ? {'callback': a:cb} : {'callback': 'coqtail#defaultCB'} return [1, coqtail#panels#getvar('coqtail_chan').sendexpr(l:args, l:opts)] else " Sync " Don't wait for interrupt to return let l:opts = a:cmd ==# 'interrupt' ? {'timeout': 0} : {} let l:res = coqtail#panels#getvar('coqtail_chan').evalexpr(l:args, l:opts) return type(l:res) == g:coqtail#compat#t_dict \ ? [l:res.buf == b:coqtail_panel_bufs.main, l:res.ret] \ : [0, -1] endif endfunction " Enable proof diffs upon starting. function! s:init_proof_diffs(coq_version) abort let l:proof_diffs_arg = coqtail#util#getvar([b:, g:], 'coqtail_auto_set_proof_diffs', '') if l:proof_diffs_arg ==# '' return endif if coqtail#version#atleast(a:coq_version, '8.9.*') call s:call('query', '', 0, { \ 'args': ['Set', 'Diffs', '"' . l:proof_diffs_arg . '"'], \ 'silent': 1}) endif endfunction " Unlock the buffer if there's no pending command and print any error messages. function! coqtail#defaultCB(chan, msg) abort let l:pending = getbufvar(a:msg.buf, 'coqtail_cmds_pending') call setbufvar(a:msg.buf, 'coqtail_cmds_pending', l:pending - 1) if l:pending - 1 == 0 call setbufvar(a:msg.buf, '&modifiable', 1) endif if a:msg.ret != v:null call coqtail#util#err(a:msg.ret) endif endfunction " Initialize Python interface. function! coqtail#init() abort if s:port == -1 let s:port = py3eval(printf( \ 'CoqtailServer.start_server(bool(%d))', \ !g:coqtail#compat#has_channel)) augroup coqtail#StopServer autocmd! * autocmd VimLeavePre * \ call py3eval('CoqtailServer.stop_server()') | let s:port = -1 augroup END " Clear Coqtail highlights when window shows an unrelated buffer. augroup coqtail#CleanupHighlights autocmd! * autocmd BufEnter * call coqtail#panels#cleanuphl() augroup END endif if !s:initted() " Since we are initializing, we are in the main buffer; " the other buffers have not been initialized yet. " Thus, we can safely refer to buffer-local b: variables let b:coqtail_cmds_pending = 0 " Open channel with Coqtail server let b:coqtail_chan = coqtail#channel#new() call b:coqtail_chan.open('localhost:' . s:port) if b:coqtail_chan.status() !=# 'open' call coqtail#util#err( \ printf('Failed to connect to Coqtail server at port %d.', s:port)) return 0 endif " Prepare auxiliary panels call coqtail#panels#init() " Shutdown the Coqtop interface when the last instance of this buffer is " closed augroup coqtail#Quit autocmd! * autocmd QuitPre \ if len(win_findbuf(expand(''))) == 1 | call coqtail#stop() | endif augroup END endif return 1 endfunction " Launch Coqtop and open the auxiliary panels. function! coqtail#start(...) abort if s:running() call coqtail#util#warn('Coq is already running.') else " See comment in coqtail#init() about buffer-local variables let b:coqtail_started = coqtail#init() if !b:coqtail_started call coqtail#stop() return 0 endif " Locate Coq project files let [b:coqtail_project_files, l:proj_args] = coqtail#coqproject#locate() " Open auxiliary panels call coqtail#panels#open(0) " Launch Coqtop let [l:ok, l:ver_or_msg] = s:call('start', 'sync', 0, { \ 'coq_path': expand(coqtail#util#getvar([b:, g:], 'coqtail_coq_path', $COQBIN)), \ 'coq_prog': coqtail#util#getvar([b:, g:], 'coqtail_coq_prog', ''), \ 'args': map(copy(l:proj_args + a:000), 'expand(v:val)')}) if !l:ok || type(l:ver_or_msg[0]) == g:coqtail#compat#t_string let l:msg = 'Failed to launch Coq.' if l:ok " l:ver_or_msg is [coqtail_error_message, coqtop_stderr] let l:msg .= "\n" . l:ver_or_msg[0] if l:ver_or_msg[1] !=# '' let l:msg .= "\n" . l:ver_or_msg[1] endif endif call coqtail#util#err(l:msg) call coqtail#stop() return 0 endif " Check if version is supported " l:ver_or_msg[0] is " {version: [major, minor, patch], str_version: str, latest: str | None} let b:coqtail_version = l:ver_or_msg[0] if b:coqtail_version.latest != v:null call coqtail#util#warn(printf( \ s:unsupported_msg, \ b:coqtail_version.str_version, \ b:coqtail_version.latest)) endif " Draw the logo let l:info_winid = bufwinid(b:coqtail_panel_bufs[g:coqtail#panels#info]) call s:call('splash', 'sync', 0, { \ 'version': b:coqtail_version.str_version, \ 'width': winwidth(l:info_winid), \ 'height': winheight(l:info_winid)}) call coqtail#refresh() call s:init_proof_diffs(b:coqtail_version.str_version) " Sync edits to the buffer, close and restore the auxiliary panels augroup coqtail#Sync autocmd! * autocmd InsertEnter call s:call('sync', 'sync', 0, {}) autocmd BufWinLeave call coqtail#panels#hide() autocmd BufWinEnter \ call coqtail#panels#open(0) | call coqtail#refresh() autocmd WinNew call coqtail#refresh() augroup END endif return 1 endfunction " Stop the Coqtop interface and clean up auxiliary panels. function! coqtail#stop() abort call s:call('stop', 'sync', 1, {}) call s:cleanup() endfunction " Advance/rewind Coq to the specified position. function! coqtail#toline(line, admit) abort " If no line was given then use the cursor's position, " otherwise use the last column in the line call s:call('to_line', '', 0, { \ 'line': (a:line == 0 ? line('.') : a:line) - 1, \ 'col': (a:line == 0 ? col('.') : len(getline(a:line))) - 1, \ 'admit': a:admit}) endfunction " Move the cursor to the specified target: " - "endpoint": the end of the region checked by Coq " - "errorpoint": the start of the error region function! coqtail#jumpto(target) abort let l:panel = coqtail#panels#switch(g:coqtail#panels#main) if l:panel == g:coqtail#panels#none " Failed to switch to main panel return endif let [l:ok, l:pos] = s:call(a:target, 'sync', 0, {}) if l:ok && type(l:pos) == g:coqtail#compat#t_list normal! m' call cursor(l:pos) endif endfunction " Refresh the auxiliary panels. function! coqtail#refresh() abort call s:call('refresh', '', 0, {}) endfunction " Define Coqtail commands with the correct options. let s:cmd_opts = { \ 'CoqStart': '-bar -nargs=* -complete=file', \ 'CoqStop': '-bar', \ 'CoqInterrupt': '-bar', \ 'CoqNext': '-bar -count=1', \ 'CoqUndo': '-bar -count=1', \ 'CoqToLine': '-bar -count=0', \ 'CoqOmitToLine': '-bar -count=0', \ 'CoqToTop': '-bar', \ 'CoqJumpToEnd': '-bar', \ 'CoqJumpToError': '-bar', \ 'CoqGotoDef': '-bang -nargs=1', \ 'Coq': '-nargs=+ -complete=custom,s:querycomplete', \ 'CoqRestorePanels': '-bar', \ 'CoqGotoGoal': '-bar -bang -count=1', \ 'CoqGotoGoalNext': '-bar -bang', \ 'CoqGotoGoalPrev': '-bar -bang', \ 'CoqToggleDebug': '-bar' \} function! s:cmddef(name, act, precmd) abort " Start Coqtail first if needed let l:act = { \ '_': a:act, \ 's': printf('if s:running() || coqtail#start() | %s | endif', a:act), \ 'i': printf('if s:initted() || coqtail#init() | %s | endif', a:act) \}[a:precmd ==# '' ? '_' : a:precmd] execute printf('command! -buffer %s %s %s', s:cmd_opts[a:name], a:name, l:act) endfunction " Define Coqtail commands. function! coqtail#define_commands() abort call s:cmddef('CoqStart', 'call coqtail#start()', '') call s:cmddef('CoqStop', 'call coqtail#stop()', '') call s:cmddef('CoqInterrupt', 'call s:call("interrupt", "sync", 0, {})', '') call s:cmddef('CoqNext', 'call s:call("step", "", 0, {"steps": })', 's') call s:cmddef('CoqUndo', 'call s:call("rewind", "", 0, {"steps": })', 's') call s:cmddef('CoqToLine', 'call coqtail#toline(, 0)', 's') call s:cmddef('CoqOmitToLine', 'call coqtail#toline(, 1)', 's') call s:cmddef('CoqToTop', 'call s:call("to_top", "", 0, {})', 's') call s:cmddef('CoqJumpToEnd', 'call coqtail#jumpto("endpoint")', 's') call s:cmddef('CoqJumpToError', 'call coqtail#jumpto("errorpoint")', 's') call s:cmddef('CoqGotoDef', 'call coqtail#gotodef(, 0)', 's') call s:cmddef('Coq', 'call s:call("query", "", 0, {"args": []})', 's') call s:cmddef('CoqRestorePanels', \ 'call coqtail#panels#open(1) | call coqtail#refresh()', 's') call s:cmddef('CoqGotoGoal', 'call coqtail#gotogoal(, 1)', 's') call s:cmddef('CoqGotoGoalNext', 'call coqtail#gotogoal(-1, 1)', 's') call s:cmddef('CoqGotoGoalPrev', 'call coqtail#gotogoal(-2, 1)', 's') call s:cmddef('CoqToggleDebug', 'call s:call("toggle_debug", "", 1, {})', 'i') endfunction " Define and default mappings for Coqtail commands. function! coqtail#define_mappings() abort nnoremap CoqStart :CoqStart nnoremap CoqStop :CoqStop nnoremap CoqInterrupt :CoqInterrupt nnoremap CoqNext :execute v:count1 'CoqNext' nnoremap CoqUndo :execute v:count1 'CoqUndo' nnoremap CoqToLine :execute v:count 'CoqToLine' nnoremap CoqOmitToLine :execute v:count 'CoqOmitToLine' nnoremap CoqToTop :CoqToTop nnoremap CoqJumpToEnd :CoqJumpToEnd nnoremap CoqJumpToError :CoqJumpToError inoremap CoqNext :CoqNext inoremap CoqUndo :CoqUndo inoremap CoqToLine :CoqToLine inoremap CoqOmitToLine :CoqOmitToLine inoremap CoqToTop :CoqToTop inoremap CoqJumpToEnd :CoqJumpToEnd inoremap CoqJumpToError :CoqJumpToError nnoremap CoqGotoDef :CoqGotoDef =coqtail#util#getcurword() nnoremap CoqSearch :Coq Search =coqtail#util#getcurword() nnoremap CoqCheck :Coq Check =coqtail#util#getcurword() nnoremap CoqAbout :Coq About =coqtail#util#getcurword() nnoremap CoqPrint :Coq Print =coqtail#util#getcurword() nnoremap CoqLocate :Coq Locate =coqtail#util#getcurword() xnoremap CoqSearch :Coq Search =coqtail#util#getvisual() xnoremap CoqCheck :Coq Check =coqtail#util#getvisual() xnoremap CoqAbout :Coq About =coqtail#util#getvisual() xnoremap CoqPrint :Coq Print =coqtail#util#getvisual() xnoremap CoqLocate :Coq Locate =coqtail#util#getvisual() nnoremap CoqRestorePanels :CoqRestorePanels nnoremap CoqGotoGoalStart :execute v:count1 'CoqGotoGoal' nnoremap CoqGotoGoalEnd :execute v:count1 'CoqGotoGoal!' nnoremap CoqGotoGoalNextStart :CoqGotoGoalNext nnoremap CoqGotoGoalNextEnd :CoqGotoGoalNext! nnoremap CoqGotoGoalPrevStart :CoqGotoGoalPrev nnoremap CoqGotoGoalPrevEnd :CoqGotoGoalPrev! nnoremap CoqToggleDebug :CoqToggleDebug " Use default mappings unless user opted out if get(g:, 'coqtail_nomap', 0) return endif let l:imap = !get(g:, 'coqtail_noimap', 0) " Use custom mapping prefix if set let l:map_prefix = get(g:, 'coqtail_map_prefix', 'c') let l:imap_prefix = get(g:, 'coqtail_imap_prefix', l:map_prefix) let l:maps = { \ 'Start': ['c', 'n'], \ 'Stop': ['q', 'n'], \ 'Interrupt': ['!', 'n'], \ 'Next': ['j', 'ni'], \ 'Undo': ['k', 'ni'], \ 'ToLine': ['l', 'ni'], \ 'ToTop': ['T', 'ni'], \ 'JumpToEnd': ['G', 'ni'], \ 'JumpToError': ['E', 'ni'], \ 'GotoDef': ['gd', 'n'], \ 'Search': ['s', 'nx'], \ 'Check': ['h', 'nx'], \ 'About': ['a', 'nx'], \ 'Print': ['p', 'nx'], \ 'Locate': ['f', 'nx'], \ 'RestorePanels': ['r', 'ni'], \ 'GotoGoalStart': ['gg', 'ni'], \ 'GotoGoalEnd': ['gG', 'ni'], \ 'GotoGoalNextStart': ['!]g', 'n'], \ 'GotoGoalNextEnd': ['!]G', 'n'], \ 'GotoGoalPrevStart': ['![g', 'n'], \ 'GotoGoalPrevEnd': ['![G', 'n'], \ 'ToggleDebug': ['d', 'n'] \} " Use v1.5 mappings let l:compat15 = index(get(g:, 'coqtail_version_compat', []), '1.5') != -1 if l:compat15 let l:maps15 = { \ 'GotoDef': ['g', 'n'], \ 'GotoGoalEnd': ['GG', 'ni'], \ 'GotoGoalNextStart': ['!g]', 'n'], \ 'GotoGoalNextEnd': ['!G]', 'n'], \ 'GotoGoalPrevStart': ['!g[', 'n'], \ 'GotoGoalPrevEnd': ['!G[', 'n'] \} let l:maps = extend(l:maps, l:maps15, 'force') endif for [l:cmd, l:info] in items(l:maps) let [l:key, l:types] = l:info let l:cmd = 'Coq' . l:cmd for l:type in split(l:types, '\zs') if !hasmapto(l:cmd, l:type) && (l:type !=# 'i' || l:imap) let l:prefix = l:type ==# 'i' ? l:imap_prefix : l:map_prefix if l:key[0] ==# '!' let l:key = l:key[1:] let l:prefix = '' endif execute printf('%smap %s%s %s', l:type, l:prefix, l:key, l:cmd) endif endfor endfor if exists('*CoqtailHookDefineMappings') call CoqtailHookDefineMappings() endif endfunction " Initialize buffer local variables, commands, and mappings. " Called from ftplugin/coq.vim, from the main buffer, meaning we can safely " refer to b: vars here. function! coqtail#register() abort " Initialize once if !exists('b:coqtail_chan') let b:coqtail_chan = 0 let b:coqtail_started = 0 let b:coqtail_timeout = 0 let b:coqtail_log_name = '' " Only define commands + mappings for main buffer for now; " these will be redefined for the goal and info buffers " when those are created (when :CoqStart is called) call coqtail#define_commands() call coqtail#define_mappings() endif endfunction ))))entry(namecinode(type directoryentry(namecoq.nixnode(typeregularcontentsó{ pkgs ? import { }, version ? null, tox_version ? null }: with builtins; assert version != null || tox_version != null; let url_8_4 = "https://github.com/NixOS/nixpkgs/archive/18.03.tar.gz"; dot_version = if version != null then version else concatStringsSep "." (filter (s: s != "") (match "coq([0-9]|master)([0-9]*)-.*" tox_version)); in if dot_version == "8.4" then (import (fetchTarball url_8_4) { }).coq_8_4 else pkgs.coq.override ({ version = dot_version; }) ))entry(namevim.nixnode(typeregularcontents^{ pkgs ? import { }, version }: with pkgs; let python = python36; vimSrc = { "7.4" = { patch = "2367"; sha256 = "sha256-M/otUhUfKEqIMdsm4vdJKjBcWPo/CokSqwKTHaAeauQ="; }; "8.0" = { patch = "1850"; sha256 = "sha256-YNYKp1KWGsQ+LghcgneHYXXd1yKdMLVnEV4w+woyw5o="; }; "8.1" = { patch = "2424"; sha256 = "sha256-uQAbLYfq6Fyittic7YzjU17vUYTuhvNHgkvOUi5xNbU="; }; "8.2" = { patch = "5172"; sha256 = "sha256-ycp9K7IpXBFLE9DV9/iQ+N1H7EMD/tP/KGv2VOXoDvE="; }; "9.0" = { patch = "2190"; sha256 = "sha256-U2zRIJssBO8PcludMn7h25XsTBgypU/WcshSmiFVdmg="; }; "9.1" = { patch = "0059"; sha256 = "sha256-68PhcTlCJ0wVFZ0Rnx8ckOe/fjwQuQMH1Eu3pyCH35A="; }; }.${version}; in stdenv.mkDerivation { name = "vim-${version}.${vimSrc.patch}"; src = with vimSrc; fetchTarball { url = "https://github.com/vim/vim/archive/v${version}.${patch}.tar.gz"; inherit sha256; }; buildInputs = [ ncurses python ]; configureFlags = [ "--with-features=huge" "--enable-python3interp=yes" "--with-python3-config-dir=${python}/lib" "--with-python3-command=${python}/bin/python" "--disable-pythoninterp" "--disable-gui" "--enable-fail-if-missing" ]; enableParallelBuilding = true; hardeningDisable = [ "fortify" ]; } ))))entry(namedocnode(type directoryentry(name coqtail.txtnode(typeregularcontentsT5*coqtail.txt* Interactive Coq Proofs in Vim Author: Wolf Honore License: MIT (see LICENSE) Coqtail provides an interface to Coqtop to enable interactive Coq proof development. Coqtail uses a separate instance of Coqtop for each buffer, so you can have multiple open Coq sessions and switch between them seamlessly using standard Vim methods (e.g., the |argument-list| or |buffer-list|). 1. Starting and Stopping Coqtail |coqtail-start-stop| 2. Movement Commands |coqtail-movement| 3. Coq Queries |coqtail-queries| 4. Panel Management |coqtail-panels| 5. Configuration |coqtail-configuration| 6. Backwards Compatibility |coqtail-backwards-compatibility| 7. Debugging |coqtail-debug| ============================= Starting and Stopping Coqtail *coqtail-start-stop* *cc* *:CoqStart* *coqtail-start* :CoqStart or cc Start the plugin. Spawn Coqtop in the background and open two windows on the right of the screen for the Goal and Info panels. *cq* *:CoqStop* *coqtail-stop* :CoqStop or cq Stop the plugin. Stop Coqtop and close the Goal and Info panels. *CTRL-C* *:CoqInterrupt* *coqtail-interrupt* :CoqInterrupt or CTRL-C Send SIGINT to Coqtop and clear any pending commands. ================= Movement Commands *coqtail-movement* *cj* *i_cj* *:CoqNext* *coqtail-next* :[count]CoqNext or [count]cj Submit the next [count] sentences to Coqtop for checking. If successful, highlight the sentences and update the Goal and Info panels accordingly. Otherwise, highlight the error and display the error message in the Info panel. [count] default: 1. *ck* *i_ck* *:CoqUndo* *coqtail-undo* :[count]CoqUndo or [count]ck Rewind by [count] steps. Un-highlight the previous sentences and update the Goal and Info panels. [count] default: 1. *cl* *i_cl* *:CoqToLine* *coqtail-to-line* :[count]CoqToLine or [count]cl Check/rewind all sentences up to the end of line [count]. If no [count] is given, use the cursor position instead. For example, given the line below, where '^' represents the cursor position, `:CoqToLine` will position the end of the checked section just after '1' whereas `:27CoqToLine` will put it after '2'. > line 27: Let x := 1.^Let y := 2. < You can use this command to clear the error highlighting for a failed sentence. The cursor has to be moved inside the sentence first, for instance by using `:CoqJumpToError` first. *:CoqOmitToLine* *coqtail-omit-to-line* :[count]CoqOmitToLine Behaves the same as `:CoqToLine`, but the bodies of all opaque proofs (those ending with "Qed" or "Admitted") are omitted and admitted. This can be useful for quickly jumping to a point towards the end of a large file. The beginnings and ends of omitted proofs (i.e., the "Proof" and "Qed"/"Admitted" commands) are marked by highlighting them with the `CoqtailOmitted` group. NOTE: Proofs must begin with "Proof" or "Proof using". NOTE: A proof is considered opaque only if every nested proof it contains is also opaque. NOTE: Proofs inside sections may need to list the variables they depend on with `Proof using` in order to get the right type when the proof body is omitted. See https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Proof-using. *cT* *i_cT* *:CoqToTop* *coqtail-to-top* :CoqToTop or cT Rewind to the top of the file. Unlike `:1CoqToLine` it rewinds to the beginning of the line. *cG* *:CoqJumpToEnd* *coqtail-jump-to-end* :CoqJumpToEnd or cG Move the cursor to the end of the checked region. This does not move the checked region. *cE* *:CoqJumpToError* *coqtail-jump-to-error* :CoqJumpToError or cE Move the cursor to the start of the error region. This does not move the checked region. *cgd* *:CoqGotoDef* *coqtail-goto-def* :CoqGotoDef[!] {arg} cgd Populate the |quickfix| list with possible locations of the definition of a Coq term and try to jump to the first one. If jumping is impossible open the |quickfix-window| instead. The first version uses {arg}, while the second uses the term under the cursor. If 'tagfunc' is supported and `g:coqtail_tagfunc` is true then the usual tag commands will also work (`:tag`, `CTRL-]`, etc). =========== Coq Queries *coqtail-queries* *:Coq* *coqtail-query* :Coq {args} Send an arbitrary query to Coqtop and write the response to the Info panel. Commands and mappings for the common queries are listed below. *cs* *coqtail-search* :Coq Search {arg} cs The first version uses {arg}, while the second uses the term under the cursor or the highlighted range in visual mode. *ch* *coqtail-check* :Coq Check {arg} ch *ca* *coqtail-about* :Coq About {arg} ca *cp* *coqtail-print* :Coq Print {arg} cp *cf* *coqtail-locate* :Coq Locate {arg} cf ================ Panel Management *coqtail-panels* *cr* *:CoqRestorePanels* *coqtail-restore-panels* :CoqRestorePanels cr Re-open the Goal and Info panels in their original configuration. *cgg* *:CoqGotoGoal* *coqtail-goto-goal-start* :[count]CoqGotoGoal cgg Scroll the Goal panel to the start of goal [count]. Control the number of goal lines to display with `g:coqtail_goal_lines`. [count] default: 1. *cgG* *:CoqGotoGoal!* *coqtail-goto-goal-end* :[count]CoqGotoGoal! cgG Same as `:CoqGotoGoal` but scroll to the end of the goal. *]g* *:CoqGotoGoalNext* *coqtail-goto-goal-next-start* :CoqGotoGoalNext ]g Scroll the Goal panel to the start of the next goal. *]G* *:CoqGotoGoalNext!* *coqtail-goto-goal-next-end* :CoqGotoGoalNext! ]G Scroll the Goal panel to the end of the next goal. *[g* *:CoqGotoGoalPrev* *coqtail-goto-goal-prev-start* :CoqGotoGoalPrev [g Scroll the Goal panel to the start of the previous goal. *[G* *:CoqGotoGoalPrev!* *coqtail-goto-goal-prev-end* :CoqGotoGoalPrev! [G Scroll the Goal panel to the end of the previous goal. ============= Configuration *coqtail-configuration* *g:coqtail_coq_path* *b:coqtail_coq_path* *coqtail-coq-path* g:coqtail_coq_path b:coqtail_coq_path The path to search for the coq(ide)top(.opt) binary. Defaults to $COQBIN, and if that is empty then $PATH is used. Default: $COQBIN *g:coqtail_coq_prog* *b:coqtail_coq_prog* *coqtail-coq-prog* g:coqtail_coq_prog b:coqtail_coq_prog The name of the Coq executable to run. If empty then it defaults to coqtop or coqidetop depending on the Coq version. For example, to use the HoTT library: > let b:coqtail_coq_path = '/path/to/HoTT' let b:coqtail_coq_prog = 'hoqidetop' < Default: '' *g:coqtail_goal-lines* *coqtail-goal-lines* g:coqtail_goal_lines The number of lines from the start of a goal to display. Used by `:CoqGotoGoal`. Default: 5. *b:coqtail_timeout* *coqtail-timeout* b:coqtail_timeout The time in seconds before interrupting Coqtop after issuing a command. A value of 0 disables the timeout. Coqtail can also be manually interrupted with `:CoqInterrupt`. Default: 0 *g:coqtail_project_names* *coq-project-files* g:coqtail_project_names The names of Coq project files to search for. The search begins in the current directory and proceeds upwards. If found, project files are parsed and passed as arguments to Coqtop by `:CoqStart`. Default: ['_CoqProject'] *b:coqtail_project_files* b:coqtail_project_files Paths to the Coq project files found during `:CoqStart`. *g:coqtail_map_prefix* *coqtail-mapping-prefix* g:coqtail_map_prefix The character(s) to begin Coqtail mappings. Default: 'c' *g:coqtail_imap_prefix* *coqtail-insert-mapping-prefix* g:coqtail_imap_prefix The character(s) to begin Coqtail insert-mode mappings. Takes precedence over `g:coqtail_map_prefix`. Default: `g:coqtail_map_prefix` *g:coqtail_nomap* *coqtail-no-mapping* g:coqtail_nomap If true then don't set any default mappings for Coqtail commands. Specific mappings can also be overwritten by defining new mappings for the desired commands. The defaults will continue to be used for the rest. Default: 0 *g:coqtail_noimap* *coqtail-no-insert-mapping* g:coqtail_noimap If true then don't set insert-mode mappings for Coqtail commands. Default: 0 *g:coqtail_nosyntax* *coqtail-no-syntax* g:coqtail_nosyntax If true then don't load the syntax script included with Coqtail. Default: 0 *g:coqtail_noindent* *coqtail-no-indent* g:coqtail_noindent If true then don't load the indent script included with Coqtail. Default: 0 *g:coqtail_noindent_comment* *coqtail-no-indent-comment* g:coqtail_noindent_comment If true then don't auto-indent within comments. Default: 0 *g:coqtail_match_shift* *coqtail-match-shift* g:coqtail_match_shift A multiple of 'shiftwidth' to indent lines after a match branch. Also applies to `Inductive` constructors. Note: This is does not affect the indentation of the line with `|` itself. For matches these are always aligned with the `match` keyword, and for `Inductive` (and related keywords) this is controlled by `g:coqtail_inductive_shift`. E.g. > match b with | true => 1 (* g:coqtail_match_shift = 1 *) | false => 2 (* g:coqtail_match_shift = 2 *) end Inductive X := | A : X (* g:coqtail_match_shift = 1 *) | B : X (* g:coqtail_match_shift = 2 *) < Default: 2 *g:coqtail_inductive_shift* *coqtail-inductive-shift* g:coqtail_inductive_shift A multiple of 'shiftwidth' to indent branches of an `Inductive` (and related keywords) constructor. E.g. > Inductive X := | A : X (* g:coqtail_inductive_shift = 1 *) | B : X (* g:coqtail_inductive_shift = 0 *) < Default: 1 *g:coqtail_indent_on_dot* *coqtail-indent-on-dot* g:coqtail_indent_on_dot If true then trigger auto-indentation when a '.' is typed. Default: 0 *g:coqtail_auto_set_proof_diffs* *b:coqtail_auto_set_proof_diffs* *coqtail-proof-diffs* g:coqtail_auto_set_proof_diffs b:coqtail_auto_set_proof_diffs The argument to automatically pass to `:Coq Set Diffs` on every new Coqtail session. For example, if `g:coqtail_auto_set_proof_diffs` is `'on'` then `:CoqStart` calls `:Coq Set Diffs "on"` immediately after launching Coqtop. The argument is ignored if it is set to `''` (the default) or if using a version of Coq that does not support proof diffs. Note: Changing this option after `:CoqStart` has no effect on the current proof. To manually toggle diffs mid-proof use `:Coq Set Diffs "{arg}"` where `{arg}` is `on`, `off`, or `removed`. Default: '' *g:coqtail_update_tagstack* *coqtail-update-tagstack* g:coqtail_update_tagstack If true then update the |tagstack| when `:CoqGotoDef` jumps to a definition. Default: 1 *g:coqtail_tagfunc* *coqtail-tagfunc* g:coqtail_tagfunc If true then set 'tagfunc' to `coqtail#gettags`. Default: 1 *g:coqtail_treat_stderr_as_warning* *coqtail-treat-stderr-as-warning* g:coqtail_treat_stderr_as_warning If true then assume all messages received from Coq on stderr are only warnings. Warnings are reported in the Info panel, but do not prevent checking subsequent sentences. This shouldn't be necessary in most cases as Coqtail can automatically recognize warning messages that follow a standard format, and generally, messages should be sent via the XML protocol rather than stderr. Default: 0 ======================= Backwards Compatibility *coqtail-backwards-compatibility* *g:coqtail_version_compat* *coqtail-version-compat* g:coqtail_version_compat New versions of Coqtail should generally maintain backwards compatibility with old ones, but in cases where they do not the old behaviors can be enabled by including the correct version string in the `g:coqtail_version_compat` list. The table below lists the valid version strings and their effects. Default: [] Version Effect~ *coqtail-version-compat-1.5* '1.5' Undo the changes to the default mappings made in v1.6. ========= Debugging *coqtail-debug* *cd* *:CoqToggleDebug* *coqtail-toggle-debug* :CoqToggleDebug cd Enable or disable logging of debugging statements to a file. Enabling creates a temporary file and displays the name in the Info panel. The name is also stored in `b:coqtail_log_name`. Disabling and enabling again creates a new log file. Disabled initially. *b:coqtail_log_name* *coqtail-log-name* b:coqtail_log_name The name of the debugging log file. Set automatically by enabling/disabling debugging with `:CoqToggleDebug`. Default: '' vim:tw=78:ts=8:ft=help:norl:noet ))))entry(nameftdetectnode(type directoryentry(namecoq.vimnode(typeregularcontents+au BufRead,BufNewFile *.v set filetype=coq ))))entry(nameftpluginnode(type directoryentry(namecoq.vimnode(typeregularcontentsą " Only source once. if exists('b:did_ftplugin') finish endif let b:did_ftplugin = 1 let b:undo_ftplugin = [] if g:coqtail#supported call coqtail#register() endif " Comments if has('comments') setlocal commentstring=(*%s*) setlocal comments=srn:(*,mb:*,ex:*) " NOTE: The 'r' and 'o' flags mistake the '*' bullet as a middle comment and " will automatically add an extra one after , 'o' or 'O'. setlocal formatoptions-=t formatoptions-=r formatoptions-=o formatoptions+=cql let b:undo_ftplugin = add(b:undo_ftplugin, 'setl cms< com< fo<') endif " Follow imports if g:coqtail#supported setlocal includeexpr=coqtail#findlib(v:fname) setlocal suffixesadd=.v setlocal include=\\\\(\\_s*\\(Import\\\|Export\\)\\>\\)\\? let b:undo_ftplugin = add(b:undo_ftplugin, 'setl inex< sua< inc<') endif " Tags if exists('+tagfunc') && g:coqtail#supported && get(g:, 'coqtail_tagfunc', 1) setlocal tagfunc=coqtail#gettags let b:undo_ftplugin = add(b:undo_ftplugin, 'setl tfu<') endif " matchit/matchup patterns if (exists('g:loaded_matchit') || exists('g:loaded_matchup')) && !exists('b:match_words') let b:match_ignorecase = 0 let s:proof_starts = ['Proof', 'Next\_s\+Obligation', 'Obligation\_s\+\d\+'] let s:proof_ends = ['Qed', 'Defined', 'Admitted', 'Abort', 'Save'] let s:proof_start = '\%(' . join(map(s:proof_starts, '"\\<" . v:val . "\\>"'), '\|') . '\)' let s:proof_end = '\%(' . join(map(s:proof_ends, '"\\<" . v:val . "\\>"'), '\|') . '\)' let b:match_words = join([ \ '\:\:\', \ '\:\', \ '\<\%(lazy\|multi\)\?match\>:\:\', \ '\%(\\|\\):\', \ s:proof_start . ':' . s:proof_end \], ',') let b:undo_ftplugin = add(b:undo_ftplugin, 'unlet! b:match_ignorecase b:match_words') endif " endwise if exists('g:loaded_endwise') let b:endwise_addition = '\=submatch(0) =~# "match" ? "end." : "End " . submatch(0) . "."' let b:endwise_words = 'Section,Module,\%(lazy\|multi\)\?match' let s:section_pat = '\<\%(Section\|Module\)\_s\+\%(\\_s\+\)\?\zs\S\+\ze\_s*\.' let s:match_pat = '\<\%(lazy\|multi\)\?match\>' let b:endwise_pattern = '\%(' . s:section_pat . '\|' . s:match_pat . '\)' let b:endwise_syngroups = 'coqVernacCmd,coqKwd,coqLtac' unlet! b:endwise_end_pattern let b:undo_ftplugin = add( \ b:undo_ftplugin, \ 'unlet! b:endwise_addition b:endwise_words b:endwise_pattern b:endwise_syngroups') endif let b:undo_ftplugin = join(b:undo_ftplugin, ' | ') ))))entry(nameindentnode(type directoryentry(namecoq.vimnode(typeregularcontents,." Vim indent file " Language: Coq " Maintainer: Vincent Aravantinos " Thanks: Some functions were inspired by the ocaml indent file " written by Jean-Francois Yuen, Mike Leary and Markus Mottl " Last Change: 2007 Dec 2 - Bugfix. " 2007 Nov 28 - Handle proofs that do not start with 'Proof'. " 2007 Nov 27 - Initial version. " Modified By: Wolf Honore " Only load this indent file when no other was loaded and user didn't opt out. if exists('b:did_indent') || get(g:, 'coqtail_noindent', 0) finish endif let b:did_indent = 1 setlocal indentexpr=GetCoqIndent() setlocal indentkeys=o,O,0=end,0=End,0=in,0=\|,0=Qed,0=Defined,0=Abort,0=Admitted,0},0),0-,0+,0<*>,0--,0++,0<*><*>,0---,0+++,0<*><*><*> if get(g:, 'coqtail_indent_on_dot', 0) setlocal indentkeys+=. endif setlocal expandtab setlocal nolisp setlocal nosmartindent setlocal shiftwidth=2 setlocal tabstop=2 let b:undo_indent = 'setl et< inde< indk< lisp< si< sw< ts<' " Only define the function once. if exists('*GetCoqIndent') finish endif " Some useful patterns let s:vernac = '\C\<\%(Abort\|About\|Add\|Admitted\|Arguments\|Axiom\|Back\|Bind\|Canonical\|Cd\|Check\|Class\|Close\|Coercion\|CoFixpoint\|CoInductive\|Combined\|Conjecture\|Context\|Corollary\|Declare\|Defined\|Definition\|Delimit\|Derive\|Drop\|End\|Eval\|Example\|Existential\|Export\|Extract\|Extraction\|Fact\|Fixpoint\|Focus\|Function\|Functional\|Goal\|Hint\|Hypothes[ie]s\|Identity\|Implicit\|Import\|Inductive\|Infix\|Inspect\|Lemma\|Let\|Load\|Locate\|Ltac\|Module\|Mutual\|Notation\|Opaque\|Open\|Parameters\=\|Print\|Program\|Proof\|Proposition\|Pwd\|Qed\|Quit\|Record\|Recursive\|Remark\|Remove\|Require\|Reserved\|Reset\|Restart\|Restore\|Resume\|Save\|Scheme\|Search\%(About\|Pattern\|Rewrite\)\=\|Section\|Set\|Show\|Structure\|SubClass\|Suspend\|Tactic\|Test\|Theorem\|Time\|Transparent\|Undo\|Unfocus\|Unset\|Variables\?\|Whelp\|Write\)\>' let s:tactic = '\C\<\%(absurd\|apply\|assert\|assumption\|auto\|case_eq\|change\|clear\%(body\)\?\|cofix\|cbv\|compare\|compute\|congruence\|constructor\|contradiction\|cut\%(rewrite\)\?\|decide\|decompose\|dependent\|destruct\|discriminate\|do\|double\|eapply\|eassumption\|econstructor\|elim\%(type\)\?\|equality\|evar\|exact\|eexact\|exists\|f_equal\|fold\|functional\|generalize\|hnf\|idtac\|induction\|info\|injection\|instantiate\|intros\?\|intuition\|inversion\%(_clear\)\?\|lapply\|left\|move\|omega\|pattern\|pose\|proof\|quote\|red\|refine\|reflexivity\|rename\|repeat\|replace\|revert\|rewrite\|right\|ring\|set\|simple\?\|simplify_eqsplit\|split\|subst\|stepl\|stepr\|symmetry\|transitivity\|trivial\|try\|unfold\|vm_compute' let s:proofstart = '\%(\[^.]*\.' let s:proofend = '\<\%(Qed\|Defined\|Abort\|Admitted\|Save\)\>' let s:bullet = '[-+*]\+)\@!' let s:bulletline = '^\s*' . s:bullet let s:match = '\<\%(lazy\|multi\)\?match\>' let s:inductive = '\%(\%(Co\)\?Inductive\|Variant\)' let s:lineend = '\s*$' " Match syntax groups. function! s:matchsyn(line, col, syns) abort return printf( \ 'synIDattr(synID(%s, %s, 0), "name") =~? "%s"', \ a:line, \ a:col, \ join(a:syns, '\\|')) endfunction let s:skip = s:matchsyn('line(".")', 'col(".")', ['string', 'comment']) " Skipping pattern, for comments " (stolen from indent/ocaml.vim, thanks to the authors) function! s:GetLineWithoutFullComment(lnum) abort let l:lnum = prevnonblank(a:lnum - 1) let l:previousline = substitute(getline(l:lnum), '(\*.*\*)\s*$', '', '') while l:previousline =~# '^\s*$' && l:lnum > 0 let l:lnum = prevnonblank(l:lnum - 1) let l:previousline = substitute(getline(l:lnum), '(\*.*\*)\s*$', '', '') endwhile return l:lnum endfunction let s:zflag = has('patch-7.4.984') ? 'z' : '' " Indent of a previous match function! s:indent_of_previous(patt) abort " If 'z' flag isn't supported then move the cursor to the start of the line if s:zflag ==# '' let l:pos = getcurpos() call cursor(line('.'), 1) endif let l:indent = indent(search(a:patt, 'bWn' . s:zflag)) " Restore cursor if s:zflag ==# '' call setpos('.', l:pos) endif return l:indent endfunction " Indent pairs function! s:indent_of_previous_pair(pstart, pmid, pend, usecol, syns) abort let l:skip = s:matchsyn('line(".")', 'col(".")', a:syns) " NOTE: Match when cursor is inside the match. See ':h searchpair'. let l:pend = len(a:pend) > 1 ? a:pend . '\zs' : a:pend let [l:line, l:col] = searchpairpos(a:pstart, a:pmid, l:pend, 'bWn', l:skip) return a:usecol && l:line != 0 ? l:col - 1 : indent(l:line) endfunction " Search modulo strings and comments function! s:search_skip(pattern, flags, stopline) abort while 1 let l:match = search(a:pattern, a:flags, a:stopline) if l:match == 0 || !eval(s:skip) return l:match endif endwhile endfunction " Check for intervening unclosed '{' or '}' function! s:find_unclosed_bracket(start, end) abort while 1 let l:brack = s:search_skip('[{}]', 'W', a:end) if l:brack == 0 " No brackets break endif " Search for match let [l:dir, l:stop] = \ getline(l:brack)[col('.') - 1] ==# '{' ? ['', a:end] : ['b', a:start] let l:matched = searchpair('{', '', '}', l:dir . 'Wn', s:skip, l:stop) if l:matched == 0 " Unclosed bracket found break endif endwhile " Restore position call cursor(a:start, 1) return l:brack endfunction " Indent matching bullets function! s:indent_bullet(currentline) abort let l:proof_start = search(s:proofstart, 'bWn') if l:proof_start == 0 return -1 endif let l:pos = getcurpos() call cursor(line('.'), 1) let l:bullet = matchstr(a:currentline, s:bullet) let l:ind = -1 while l:ind == -1 " Find previous bullet of the same length let l:prev_bullet = search('\M^\s\*' . l:bullet . l:bullet[0] . '\@!', 'bW', l:proof_start) " If no previous ones to match, fall through and indent using another rule if l:prev_bullet == 0 break endif if s:find_unclosed_bracket(l:prev_bullet, v:lnum) " Bullets not in the same brackets, keep looking continue endif let l:ind = indent(l:prev_bullet) endwhile " Restore position call setpos('.', l:pos) return l:ind endfunction function! GetCoqIndent() abort try let l:ignorecase_save = &ignorecase let l:smartcase_save = &smartcase let l:magic_save = &magic set noignorecase nosmartcase magic return s:GetCoqIndent() finally let &ignorecase = l:ignorecase_save let &smartcase = l:smartcase_save let &magic = l:magic_save endtry endfunction " Main function function! s:GetCoqIndent() abort " Find a non-commented currentline above the current currentline. let l:lnum = s:GetLineWithoutFullComment(v:lnum) let l:ind = indent(l:lnum) let l:previousline = substitute(getline(l:lnum), '(\*.*\*)\s*$', '', '') let l:currentline = getline(v:lnum) " current line is a comment if l:currentline =~# '^\s*(\*' || eval(s:matchsyn(v:lnum, 1, ['comment'])) " ignore comments if get(g:, 'coqtail_noindent_comment', 0) return -1 endif " ignore line comments if l:currentline !~# '^\s*(\*' " current line is starting a multiline comment let l:startcom = s:indent_of_previous_pair('(\*', '', '\*)', 1, ['string']) if l:currentline =~# '^\s*\*' return l:startcom + 1 else return l:startcom + 3 endif endif endif " At the start of the file use zero indent. if l:lnum == 0 return 0 endif " previous line ends a comment if l:previousline =~# '\*)\s*$' while eval(s:matchsyn(l:lnum, 1, ['comment'])) " indent relative to the last non-comment call search('\*)', 'bW') let l:skip = s:matchsyn('line(".")', 'col(".")', ['string']) let l:startcom = searchpair('(\*', '', '\*)', 'bWn', l:skip) let l:lnum = s:GetLineWithoutFullComment(l:startcom) endwhile let l:ind = indent(l:lnum) let l:previousline = substitute(getline(l:lnum), '(\*.*\*)\s*$', '', '') if l:lnum == 0 return 0 endif endif " current line begins with '.': if l:currentline =~# '^\s*\.' return s:indent_of_previous(s:vernac) endif " current line begins with 'end': if l:currentline =~# '^\s*end\>' return s:indent_of_previous_pair(s:match, '', '\', 1, ['string', 'comment']) endif " current line begins with 'in': if l:currentline =~# '^\s*\' return s:indent_of_previous_pair('\', '', '\', 0, ['string', 'comment']) endif " current line begins with '|': if l:currentline =~# '^\s*|[|}]\@!' let l:match = s:indent_of_previous_pair(s:match, '', '\', 1, ['string', 'comment']) let l:off = get(g:, 'coqtail_inductive_shift', 1) * &sw return l:match != -1 ? l:match : s:indent_of_previous('^\s*' . s:inductive) + l:off endif " current line begins with terminating '|}', '}', or ')' if l:currentline =~# '^\s*|}' return s:indent_of_previous_pair('{|', '', '|}', 0, ['string', 'comment']) elseif l:currentline =~# '^\s*}' return s:indent_of_previous_pair('{', '', '}', 0, ['string', 'comment']) elseif l:currentline =~# '^\s*)' return s:indent_of_previous_pair('(', '', ')', 0, ['string', 'comment']) endif " end of proof if l:currentline =~# s:proofend return s:indent_of_previous(s:vernac . '\&\%(' . s:proofend . '\)\@!') endif " start of proof if l:previousline =~# s:proofstart . s:lineend return l:ind + &sw endif " bullet on current line if l:currentline =~# s:bulletline let l:ind_bullet = s:indent_bullet(l:currentline) if l:ind_bullet != -1 return l:ind_bullet endif " fall through endif " bullet on previous line if l:previousline =~# s:bulletline let l:bullet = matchstr(l:previousline, s:bullet) return l:ind + len(l:bullet) + 1 endif " } at end of previous line " NOTE: must come after the bullet cases if l:previousline =~# '}\s*$' call search('}', 'bW') return s:indent_of_previous_pair('{', '', '}', 0, ['string', 'comment']) endif " previous line begins with 'Section/Module': if l:previousline =~# '^\s*\%(Section\|Module\)\>' " don't indent if Section/Module is empty or is defined on one line if l:currentline !~# '^\s*End\>' && l:previousline !~# ':=.*\.\s*$' && l:previousline !~# '\' return l:ind + &sw endif " fall through endif " current line begins with 'End': if l:currentline =~# '^\s*End\>' let l:matches = matchlist(l:currentline, 'End\_s\+\([^.[:space:]]\+\)') if l:matches != [] let l:name = l:matches[1] return s:indent_of_previous('\%(Section\|Module\)\_s\+' . l:name) endif " fall through endif " previous line has the form '|...' if l:previousline =~# '[{|]\@1\)\@!\)*$' return l:ind + get(g:, 'coqtail_match_shift', 2) * &sw endif " previous line has '{|' or '{' with no matching '|}' or '}' if l:previousline =~# '{|\?[^}]*\s*$' return l:ind + &sw endif " unterminated vernacular sentences if l:previousline =~# s:vernac . '.*[^.[:space:]]\s*$' && l:previousline !~# '^\s*$' return l:ind + &sw endif " back to normal indent after lines ending with '.' if l:previousline =~# '\.\s*$' if eval(s:matchsyn(l:lnum, 1, ['proof', 'tactic'])) return l:ind else return s:indent_of_previous(s:vernac) endif endif " previous line ends with 'with' if l:previousline =~# '\\%(.\%(\\)\@!\)*$' return l:ind + &sw endif " else return l:ind endfunction ))))entry(namepythonnode(type directoryentry(name coqtail.pynode(typeregularcontents*į# -*- coding: utf8 -*- # Author: Wolf Honore """Classes and functions for managing auxiliary panels and Coqtop interfaces.""" import json import re import socket import threading import time from collections import defaultdict as ddict from collections import deque from concurrent import futures from itertools import count, islice, zip_longest from queue import Empty, Queue from socketserver import StreamRequestHandler, ThreadingTCPServer from typing import ( TYPE_CHECKING, Any, Callable, DefaultDict, Deque, Dict, Iterable, Iterator, List, Mapping, NamedTuple, Optional, Sequence, Tuple, TypeVar, Union, cast, overload, ) import coqtop as CT from xmlInterface import Goals, PPTag, TaggedToken T = TypeVar("T") Highlight = NamedTuple( "Highlight", [("line_no", int), ("index", int), ("tok_len", int), ("tag", PPTag)], ) ProofRange = NamedTuple( "ProofRange", (("proof", Mapping[str, Tuple[int, int]]), ("qed", Mapping[str, Tuple[int, int]])), ) Req = Tuple[int, int, str, Mapping[str, Any]] # (msg_id, bnum, func, args) Res = Tuple[int, Any] # (msg_id, data) SkipFun = Callable[[Sequence[bytes], int, int], Optional[Tuple[int, int]]] if TYPE_CHECKING: # Some types are only subscriptable during type checking. from typing_extensions import TypedDict ReqQueue = Queue[Req] ResQueue = Queue[Res] VimOptions = TypedDict( "VimOptions", { "encoding": str, "timeout": int, "filename": str, "stderr_is_warning": bool, }, ) ResFuture = futures.Future[Optional[str]] else: ReqQueue = Queue ResQueue = Queue VimOptions = Mapping[str, Any] ResFuture = futures.Future PROOF_START_PAT = re.compile(rb"^\s*(Proof)\b") PROOF_END_PAT = re.compile(rb"^\s*(Qed|Admitted|Defined|Abort|Save)\b") OPAQUE_PROOF_ENDS = {b"Qed", b"Admitted"} def lines_and_highlights( tagged_tokens: Union[str, Iterable[TaggedToken]], line_no: int, ) -> Tuple[List[str], List[Highlight]]: """Converts a sequence of tagged tokens into lines and higlight positions. Note that matchaddpos()'s highlight positions are 1-indexed, but this function expects line_no to be 0-indexed. """ # If tagged_tokens turns out to already be a string (which is the case for # older versions of Coq), just return it as is, with no highlights. if isinstance(tagged_tokens, str): return tagged_tokens.splitlines(), [] lines: List[str] = [] highlights: List[Highlight] = [] line_no += 1 # Convert to 1-indexed per matchaddpos()'s spec line, index = "", 1 for token, tag in tagged_tokens: # NOTE: Can't use splitlines or else tokens like ' =\n' won't properly # begin a new line for i, tok in enumerate(token.split("\n")): if i > 0: # Encountered a newline in token lines.append(line) line_no += 1 line, index = "", 1 tok_len = len(tok.encode("utf-8")) if tag is not None: highlights.append(Highlight(line_no, index, tok_len, tag)) line += tok index += tok_len lines.append(line) return lines, highlights class UnmatchedError(Exception): """An unmatched comment or string was found.""" def __init__(self, token: str, loc: Tuple[int, int]) -> None: super().__init__(f"Found unmatched {token}.") line, col = loc self.range = (loc, (line, col + len(token))) class NoDotError(Exception): """No more sentences were found.""" # Coqtail Server # class Coqtail: """Manage Coqtop interfaces and auxiliary buffers for each Coq file.""" def __init__(self, handler: "CoqtailHandler") -> None: """Initialize variables. coqtop - The Coqtop interface handler - The Vim interface changedtick - The most recent value of `b:changedtick` that Coqtail has observed. The positions stored in other variables (`endpoints`, `send_queue`, `error_at`) can become invalid when this value gets outdated. To protect Coqtail from this inconsistency, the buffer is locked (unset `modifiable`) when processing. When processing, `sync()` should be called first to refresh this variable and remove the positions invalidated by the new changes to the buffer. buffer - The buffer corresponding to changedtick endpoints - A stack (grows to the right) of the end positions of the sentences checked by CoqTop. The end position of a sentence is the start position of its next sentence. send_queue - A queue of the sentences to send to Coqtop. Each item contains the "start" and "end" (inclusive, including the dot) position of the sentence. error_at - The position of the last error omitted_proofs - The positions of the starts and ends of the proofs that have been skipped by `to_line()`. info_msg - Lines of text to display in the info panel goal_msg - Lines of text to display in the goal panel goal_hls - Highlight positions for each line of goal_msg """ self.coqtop = CT.Coqtop() self.handler = handler self.changedtick = 0 self.buffer: List[bytes] = [] self.endpoints: List[Tuple[int, int]] = [] self.send_queue: Deque[Mapping[str, Tuple[int, int]]] = deque() self.error_at: Optional[Tuple[Tuple[int, int], Tuple[int, int]]] = None self.omitted_proofs: List[ProofRange] = [] self.info_msg: List[str] = [] self.goal_msg: List[str] = [] self.goal_hls: List[Highlight] = [] def sync(self, opts: VimOptions) -> Optional[str]: """Check if the buffer has been updated and rewind Coqtop if so.""" err = None newtick = self.get_changedtick() if newtick != self.changedtick: newbuf = self.get_buffer() if self.endpoints != []: diff = _diff_lines(self.buffer, newbuf, self.endpoints[-1]) if diff is not None: linediff, coldiff = diff err = self.rewind_to(linediff, coldiff + 1, opts=opts) self.changedtick = newtick self.buffer = newbuf return err # Coqtop Interface # def start( self, coq_path: str, coq_prog: str, args: Iterable[str], opts: VimOptions, ) -> Tuple[Union[CT.VersionInfo, str], str]: """Start a new Coqtop instance.""" try: ver_or_err, stderr = self.coqtop.start( coq_path if coq_path != "" else None, coq_prog if coq_prog != "" else None, opts["filename"], args, timeout=opts["timeout"], stderr_is_warning=opts["stderr_is_warning"], ) self.print_stderr(stderr) except (ValueError, CT.CoqtopError) as e: ver_or_err, stderr = str(e), "" return ver_or_err, stderr def stop(self, opts: VimOptions) -> None: """Stop Coqtop.""" # pylint: disable=unused-argument # opts is always passed by handle(). self.coqtop.stop() def step(self, steps: int, opts: VimOptions) -> Optional[str]: """Advance Coq by 'steps' sentences.""" self.sync(opts=opts) if steps < 1: return None # Get the location of the last '.' line, col = self.endpoints[-1] if self.endpoints != [] else (0, 0) unmatched = None for _ in range(steps): try: to_send = _get_message_range(self.buffer, (line, col)) except UnmatchedError as e: unmatched = e break except NoDotError: break line, col = to_send["stop"] col += 1 self.send_queue.append(to_send) failed_at, err = self.send_until_fail(self.buffer, opts=opts) if unmatched is not None and failed_at is None: # Only report unmatched if no other errors occurred first self.set_info(str(unmatched), reset=False) self.error_at = unmatched.range self.refresh(goals=False, opts=opts) return err def rewind(self, steps: int, opts: VimOptions) -> Optional[str]: """Rewind Coq by 'steps' sentences.""" if steps < 1 or self.endpoints == []: return None try: _, msg, extra_steps, stderr = self.coqtop.rewind( steps, stderr_is_warning=opts["stderr_is_warning"], ) self.print_stderr(stderr) except CT.CoqtopError as e: return str(e) if extra_steps is None: return msg self.endpoints = self.endpoints[: -(steps + extra_steps)] self.omitted_proofs = [ range_ for range_ in self.omitted_proofs if self.endpoints != [] and range_.qed["stop"] <= self.endpoints[-1] ] self.error_at = None self.refresh(opts=opts) return None def to_line( self, line: int, col: int, admit: bool, opts: VimOptions, ) -> Optional[str]: """Advance/rewind Coq to the specified position.""" self.sync(opts=opts) # Get the location of the last '.' eline, ecol = self.endpoints[-1] if self.endpoints != [] else (0, 0) # Check if should rewind or advance if (line, col) < (eline, ecol): # Don't rewind the sentence whose dot is on the specified position. # vvv return self.rewind_to(line, col + 1 + 1, opts=opts) unmatched = None while True: try: to_send = _get_message_range(self.buffer, (eline, ecol)) except UnmatchedError as e: # Only report unmatched if it occurs after the desired position if e.range[0] <= (line, col): unmatched = e break except NoDotError: break if (line, col) < to_send["stop"]: break eline, ecol = to_send["stop"] ecol += 1 self.send_queue.append(to_send) failed_at, err = self.send_until_fail(self.buffer, admit=admit, opts=opts) if unmatched is not None and failed_at is None: # Only report unmatched if no other errors occurred first self.set_info(str(unmatched), reset=False) self.error_at = unmatched.range self.refresh(goals=False, opts=opts) return err def to_top(self, opts: VimOptions) -> Optional[str]: """Rewind to the beginning of the file.""" return self.rewind_to(0, 1, opts=opts) def query( self, args: Iterable[str], opts: VimOptions, silent: bool = False, ) -> None: """Forward Coq query to Coqtop interface.""" success, msg, stderr = self.do_query(" ".join(args), opts=opts) if not success or not silent: self.set_info(msg, reset=True) self.print_stderr(stderr) self.refresh(goals=False, opts=opts) def endpoint(self, opts: VimOptions) -> Tuple[int, int]: """Return the end of the Coq checked section.""" # pylint: disable=unused-argument # opts is always passed by handle(). # Get the location of the last '.' line, col = self.endpoints[-1] if self.endpoints != [] else (0, 1) return (line + 1, col - 1 + 1) def errorpoint(self, opts: VimOptions) -> Optional[Tuple[int, int]]: """Return the start of the error region.""" # pylint: disable=unused-argument # opts is always passed by handle(). if self.error_at is not None: line, col = self.error_at[0] return (line + 1, col + 1) return None # Helpers # def send_until_fail( self, buffer: Sequence[bytes], opts: VimOptions, admit: bool = False, ) -> Tuple[Optional[Tuple[int, int]], Optional[str]]: """Send all sentences in 'send_queue' until an error is encountered.""" empty = self.send_queue == deque() scroll = len(self.send_queue) > 1 failed_at = None no_msgs = True self.error_at = None admit_up_to: Optional[Mapping[str, Tuple[int, int]]] = None while self.send_queue: self.refresh(goals=False, force=False, scroll=scroll, opts=opts) to_send = self.send_queue.popleft() message = _between(buffer, to_send["start"], to_send["stop"]) no_comments, _ = _strip_comments(message) if admit: if admit_up_to is None: pstart = PROOF_START_PAT.match(no_comments) if pstart is not None: # Reached the beginning of a proof in admit mode. admit_up_to = _find_opaque_proof_end(buffer, self.send_queue) if admit_up_to is not None: admit_from = _shrink_range_to_match( to_send, pstart.group(), pstart.start(1), ) self.omitted_proofs.append( ProofRange(admit_from, admit_up_to) ) elif admit_up_to["stop"] == to_send["stop"]: # Reached the end of an opaque proof in admit mode. Replace # with `Admitted`. match = PROOF_END_PAT.match(no_comments) assert match is not None and match.group(1) in OPAQUE_PROOF_ENDS message = no_comments = b"Admitted." admit_up_to = None else: # Inside an opaque proof in admit mode. Skip this sentence. continue try: success, msg, err_loc, stderr = self.coqtop.dispatch( message.decode("utf-8"), no_comments.decode("utf-8"), encoding=opts["encoding"], timeout=opts["timeout"], stderr_is_warning=opts["stderr_is_warning"], ) except CT.CoqtopError as e: return None, str(e) if msg != "": self.set_info(msg, reset=no_msgs) no_msgs = False self.print_stderr(stderr) no_msgs = no_msgs and stderr == "" if success: line, col = to_send["stop"] self.endpoints.append((line, col + 1)) else: self.send_queue.clear() failed_at = to_send["start"] # Highlight error location assert err_loc is not None loc_s, loc_e = err_loc if loc_s == loc_e == -1: self.error_at = (to_send["start"], to_send["stop"]) else: line, col = to_send["start"] sline, scol = _pos_from_offset(col, message, loc_s) eline, ecol = _pos_from_offset(col, message, loc_e) self.error_at = ((line + sline, scol), (line + eline, ecol)) # Clear info if no messages and at least one message was sent if no_msgs and not empty: self.set_info("", reset=True) self.refresh(opts=opts, scroll=scroll) return failed_at, None def rewind_to(self, line: int, col: int, opts: VimOptions) -> Optional[str]: """Rewind to the point where all remaining endpoints are strictly before the specified position. """ # Count the number of endpoints after the specified location steps_too_far = sum(pos >= (line, col) for pos in self.endpoints) return self.rewind(steps_too_far, opts=opts) def do_query(self, query: str, opts: VimOptions) -> Tuple[bool, str, str]: """Execute a query and return the reply.""" # Ensure that the query ends in '.' if not query.endswith("."): query += "." try: success, msg, _, stderr = self.coqtop.dispatch( query, in_script=False, encoding=opts["encoding"], timeout=opts["timeout"], stderr_is_warning=opts["stderr_is_warning"], ) except CT.CoqtopError as e: return False, str(e), "" return success, msg, stderr def qual_name(self, target: str, opts: VimOptions) -> Optional[Tuple[str, str]]: """Find the fully qualified name of 'target' using 'Locate'.""" success, locate, _ = self.do_query(f"Locate {target}.", opts=opts) if not success: return None # Join lines that start with whitespace to the previous line locate = re.sub(r"\n +", " ", locate) # Choose first match from 'Locate' since that is the default in the # current context match = locate.split("\n")[0] if "No object of basename" in match: return None # Look for alias alias = re.search(r"\(alias of (.*)\)", match) if alias is not None: # Found an alias, search again using that return self.qual_name(alias.group(1), opts=opts) info = match.split() # Special case for Module Type if info[0] == "Module" and info[1] == "Type": tgt_type = "Module Type" qual_tgt = info[2] else: tgt_type, qual_tgt = info[:2] return qual_tgt, tgt_type def find_lib(self, lib: str, opts: VimOptions) -> Optional[str]: """Find the path to the .v file corresponding to the libary 'lib'.""" success, locate, _ = self.do_query(f"Locate Library {lib}.", opts=opts) if not success: return None path = re.search(r"file\s+(.*)\.vo", locate) return path.group(1) if path is not None else None def find_qual( self, qual_tgt: str, tgt_type: str, opts: VimOptions, ) -> Optional[Tuple[str, str]]: """Find the Coq file containing the qualified name 'qual_tgt'.""" qual_comps = qual_tgt.split(".") base_name = qual_comps[-1] # If 'qual_comps' starts with Top or 'tgt_type' is Variable then # 'qual_tgt' is defined in the current file if qual_comps[0] == "Top" or tgt_type == "Variable": return opts["filename"], base_name # Find the longest prefix of 'qual_tgt' that matches a logical path in # 'path_map' for end in range(-1, -len(qual_comps), -1): path = self.find_lib(".".join(qual_comps[:end]), opts=opts) if path is not None: return path + ".v", base_name return None def find_def( self, target: str, opts: VimOptions, ) -> Optional[Tuple[str, List[str]]]: """Create patterns to jump to the definition of 'target'.""" # Get the fully qualified version of 'target' qual = self.qual_name(target, opts=opts) if qual is None: return None qual_tgt, tgt_type = qual # Find what file the definition is in and what type it is tgt = self.find_qual(qual_tgt, tgt_type, opts=opts) if tgt is None: return None tgt_file, tgt_name = tgt return tgt_file, get_searches(tgt_type, tgt_name) def next_bullet(self, opts: VimOptions) -> Optional[str]: """Check the bullet expected for the next subgoal.""" success, show, _ = self.do_query("Show.", opts=opts) if not success: return None bmatch = re.search(r'(?:bullet |unfocusing with ")([-+*}]+)', show) return bmatch.group(1) if bmatch is not None else None # Goals and Infos # def refresh( self, opts: VimOptions, goals: bool = True, force: bool = True, scroll: bool = False, ) -> None: """Refresh the auxiliary panels.""" if goals: newgoals, newinfo = self.get_goals(opts=opts) if newinfo != "": self.set_info(newinfo, reset=False) if newgoals is not None: self.set_goal(self.pp_goals(newgoals, opts=opts)) else: self.set_goal(clear=True) self.handler.refresh(goals=goals, force=force, scroll=scroll) def get_goals(self, opts: VimOptions) -> Tuple[Optional[Goals], str]: """Get the current goals.""" try: _, msg, goals, stderr = self.coqtop.goals( timeout=opts["timeout"], stderr_is_warning=opts["stderr_is_warning"], ) self.print_stderr(stderr) return goals, msg except CT.CoqtopError as e: return None, str(e) def pp_goals( self, goals: Goals, opts: VimOptions, ) -> Tuple[List[str], List[Highlight]]: """Pretty print the goals.""" lines: List[str] = [] highlights: List[Highlight] = [] ngoals = len(goals.fg) nhidden = len(goals.bg[0]) if goals.bg != [] else 0 nshelved = len(goals.shelved) nadmit = len(goals.given_up) # Information about number of remaining goals lines.append(f"{ngoals} subgoal{'' if ngoals == 1 else 's'}") if nhidden > 0: lines.append(f"({nhidden} unfocused at this level)") if nshelved > 0 or nadmit > 0: line = [] if nshelved > 0: line.append(f"{nshelved} shelved") if nadmit > 0: line.append(f"{nadmit} admitted") lines.append(" ".join(line)) lines.append("") # When a subgoal is finished if ngoals == 0: next_goal = next((bgs[0] for bgs in goals.bg if bgs != []), None) if next_goal is not None: bullet = self.next_bullet(opts=opts) bullet_info = "" if bullet is not None: if bullet == "}": bullet_info = "end this goal with '}'" else: bullet_info = f"use bullet '{bullet}'" next_info = "Next goal" if next_goal.name is not None: next_info += f" [{next_goal.name}]" if bullet_info != "": next_info += f" ({bullet_info})" next_info += ":" lines += [next_info, ""] ls, hls = lines_and_highlights(next_goal.ccl, len(lines)) lines += ls highlights += hls else: lines.append("All goals completed.") for idx, goal in enumerate(goals.fg): if idx == 0: # Print the environment only for the current goal for hyp in goal.hyp: ls, hls = lines_and_highlights(hyp, len(lines)) lines += ls highlights += hls hbar = f"{'':=>25} ({idx + 1} / {ngoals})" if goal.name is not None: hbar += f" [{goal.name}]" lines += ["", hbar, ""] ls, hls = lines_and_highlights(goal.ccl, len(lines)) lines += ls highlights += hls return lines, highlights def set_goal( self, msg: Optional[Tuple[List[str], List[Highlight]]] = None, clear: bool = False, ) -> None: """Update the goal message.""" if msg is not None: self.goal_msg, self.goal_hls = msg if clear or "".join(self.goal_msg) == "": self.goal_msg, self.goal_hls = ["No goals."], [] def set_info( self, msg: Optional[Union[str, List[str]]] = None, reset: bool = True, ) -> None: """Update the info message.""" if msg is not None: info = msg.split("\n") if isinstance(msg, str) else msg if reset or self.info_msg == []: self.info_msg = info else: self.info_msg += [""] + info # Normalize an empty buffer to an empty list instead of a single # empty line. if self.info_msg == [""]: self.info_msg = [] def print_stderr(self, err: str) -> None: """Display a message from Coqtop stderr.""" if err != "": self.set_info("From stderr:\n" + err, reset=False) @property def highlights(self) -> Dict[str, Optional[Union[str, List[Tuple[int, int, int]]]]]: """Vim match patterns for highlighting.""" matches: Dict[str, Optional[Union[str, List[Tuple[int, int, int]]]]] = { "checked": None, "sent": None, "error": None, "omitted": None, } if self.endpoints != []: line, col = self.endpoints[-1] matches["checked"] = matcher[: line + 1, :col] if self.send_queue: sline, scol = self.endpoints[-1] if self.endpoints != [] else (0, -1) eline, ecol = self.send_queue[-1]["stop"] matches["sent"] = matcher[sline : eline + 1, scol:ecol] if self.error_at is not None: (sline, scol), (eline, ecol) = self.error_at matches["error"] = matcher[sline : eline + 1, scol:ecol] if self.omitted_proofs != []: ranges = [] for pstart, pend in self.omitted_proofs: for range_ in (pstart, pend): sline, scol = range_["start"] eline, ecol = range_["stop"] for line in range(sline, eline + 1): col = scol if line == sline else 0 span = ( ecol - col if line == eline else len(self.buffer[line]) - col ) ranges.append((line + 1, col + 1, span)) matches["omitted"] = ranges return matches def panels( self, goals: bool = True, ) -> Mapping[str, Tuple[List[str], List[Highlight]]]: """The auxiliary panel content.""" panels: Dict[str, Tuple[List[str], List[Highlight]]] = { "info": (self.info_msg, []) } if goals: panels["goal"] = (self.goal_msg, self.goal_hls) return panels def splash( self, version: str, width: int, height: int, opts: VimOptions, ) -> None: """Display the logo in the info panel.""" # pylint: disable=unused-argument # opts is always passed by handle(). msg = [ "~~~~~~~~~~~~~~~~~~~~~~~", "Ī» /", " Ī» Coqtail / ", " Ī» / ", f" Ī»{('Coq ' + version).center(15)}/ ", " Ī» / ", " Ī» / ", " Ī» / ", " Ī» / ", " Ī» / ", " Ī» / ", " Ī» / ", " ā€– ", " ā€– ", " ā€– ", " / Ī» ", " /___Ī» ", ] msg_maxw = max(len(line) for line in msg) msg = [line.center(width - msg_maxw // 2) for line in msg] # Center vertically if the Info panel is empty. if self.info_msg == []: msg = [""] * ((height // 2) - (len(msg) // 2 + 1)) + msg msg = [line.rstrip() for line in msg] self.set_info(msg, reset=False) def toggle_debug(self, opts: VimOptions) -> None: """Enable or disable logging of debug messages.""" log = self.coqtop.toggle_debug() if log is None: msg = "Debugging disabled." self.log = "" else: msg = f"Debugging enabled. Log: {log}." self.log = log self.set_info(msg, reset=True) self.refresh(goals=False, opts=opts) # Vim Helpers # def get_changedtick(self) -> int: """Get the value of changedtick for this buffer.""" return cast(int, self.handler.vimvar("changedtick")) @property def log(self) -> str: """The name of this buffer's debug log.""" return cast(str, self.handler.vimvar("coqtail_log_name")) @log.setter def log(self, log: str) -> None: """The name of this buffer's debug log.""" self.handler.vimvar("coqtail_log_name", log) def get_buffer(self) -> List[bytes]: """Get the contents of this buffer.""" lines: List[str] = self.handler.vimcall( "getbufline", True, self.handler.bnum, 1, "$", ) return [line.encode("utf-8") for line in lines] class CoqtailHandler(StreamRequestHandler): """Forward messages between Vim and Coqtail.""" # Redraw rate in seconds refresh_rate = 0.05 # How often to check for a closed channel check_close_rate = 1 # Is the channel open closed = False # Is a request currently being handled working = False # Is the client synchronous sync = False def parse_msgs(self) -> None: """Parse messages sent over a Vim channel.""" while not self.closed: try: msg = self.rfile.readline() msg_id, data = json.loads(msg) except (json.JSONDecodeError, ConnectionError): # Check if channel closed self.closed = True break if msg_id >= 0: # request from Vim bnum, func, args = data if func == "interrupt": self.interrupt() else: self.reqs.put((msg_id, bnum, func, args)) else: # response to a `vimeval` request # NOTE: Accessing self.resps concurrently creates a race # condition where defaultdict could construct a Queue twice with self.resp_lk: self.resps[-msg_id].put((msg_id, data)) @overload def get_msg(self, msg_id: None = ...) -> Req: ... @overload def get_msg(self, msg_id: int) -> Res: ... def get_msg(self, msg_id: Optional[int] = None) -> Union[Res, Req]: """Check for any pending messages from Vim.""" queue: Union[ReqQueue, ResQueue] if msg_id is None: queue = self.reqs else: with self.resp_lk: queue = self.resps[msg_id] while not self.closed: try: return queue.get(timeout=self.check_close_rate) except Empty: pass raise EOFError def handle(self) -> None: """Forward requests from Vim to the appropriate Coqtail function.""" self.coq = Coqtail(self) self.closed = False # Requests from Vim (`s:call`) self.reqs: ReqQueue = Queue() # Responses to `vimeval` requests. # The key is the id of Vim's request that was being handled at the # moment of `vimeval` call. self.resps: DefaultDict[int, ResQueue] = ddict(Queue) self.resp_lk = threading.Lock() threading.Thread(target=self.parse_msgs, daemon=True).start() while not self.closed: try: self.working = False self.msg_id, self.bnum, func, args = self.get_msg() self.refresh_time = 0.0 self.working = True except EOFError: break handlers: Mapping[str, Callable[..., object]] = { "start": self.coq.start, "stop": self.coq.stop, "step": self.coq.step, "rewind": self.coq.rewind, "to_line": self.coq.to_line, "to_top": self.coq.to_top, "query": self.coq.query, "endpoint": self.coq.endpoint, "errorpoint": self.coq.errorpoint, "toggle_debug": self.coq.toggle_debug, "splash": self.coq.splash, "sync": self.coq.sync, "find_def": self.coq.find_def, "find_lib": self.coq.find_lib, "refresh": self.coq.refresh, } handler = handlers.get(func, None) try: ret = handler(**args) if handler is not None else None msg = [self.msg_id, {"buf": self.bnum, "ret": ret}] self.wfile.write(_to_jsonl(msg)) except (EOFError, ConnectionError): break try: del self.resps[self.msg_id] except KeyError: pass if func == "stop": break def vimeval(self, expr: List[Any], wait: bool = True) -> Any: """Send Vim a request as `:h channel-commands`.""" if wait: expr += [-self.msg_id] self.wfile.write(_to_jsonl(expr)) if wait: msg_id, res = self.get_msg(self.msg_id) assert msg_id == -self.msg_id return res return None def vimcall(self, expr: str, wait: bool, *args: Any) -> Any: """Request Vim to evaluate a function call.""" return self.vimeval(["call", expr, args], wait=wait) def vimvar(self, var: str, val: Optional[Any] = None) -> Any: """Get or set the value of a Vim variable.""" return ( self.vimcall("getbufvar", True, self.bnum, var) if val is None else self.vimcall("setbufvar", True, self.bnum, var, val) ) def refresh( self, goals: bool = True, force: bool = True, scroll: bool = False, ) -> None: """Refresh the highlighting and auxiliary panels.""" # pylint: disable=attribute-defined-outside-init # refresh_time is defined in handle() when the connection is opened. if not force: cur_time = time.time() force = cur_time - self.refresh_time > self.refresh_rate self.refresh_time = cur_time if force: self.vimcall( "coqtail#panels#refresh", self.sync, self.bnum, self.coq.highlights, self.coq.panels(goals), scroll, ) def interrupt(self) -> None: """Interrupt Coqtop and clear the request queue.""" if self.working: self.working = False while not self.reqs.empty(): try: msg_id, bnum, _, _ = self.reqs.get_nowait() msg = [msg_id, {"buf": bnum, "ret": None}] self.wfile.write(_to_jsonl(msg)) except Empty: break self.coq.coqtop.interrupt() class CoqtailServer: """A server through which Vim and Coqtail communicate.""" serv = None @staticmethod def start_server(sync: bool) -> int: """Start the TCP server.""" # NOTE: port = 0 chooses any arbitrary open one CoqtailHandler.sync = sync CoqtailServer.serv = ThreadingTCPServer(("localhost", 0), CoqtailHandler) CoqtailServer.serv.daemon_threads = True _, port = CoqtailServer.serv.server_address threading.Thread(target=CoqtailServer.serv.serve_forever, daemon=True).start() return port @staticmethod def stop_server() -> None: """Stop the TCP server.""" if CoqtailServer.serv is not None: CoqtailServer.serv.shutdown() CoqtailServer.serv.server_close() CoqtailServer.serv = None class ChannelManager: """Emulate Vim's ch_* functions with sockets.""" pool = futures.ThreadPoolExecutor() channels: Dict[int, socket.socket] = {} results: Dict[int, ResFuture] = {} sessions: Dict[int, int] = {} ch_id = count(1) msg_id = count(1) @staticmethod def open(address: str) -> int: """Open a channel.""" ch_id = next(ChannelManager.ch_id) host, port = address.split(":") ChannelManager.channels[ch_id] = socket.create_connection((host, int(port))) return ch_id @staticmethod def close(handle: int) -> None: """Close a channel.""" try: ChannelManager.channels[handle].close() del ChannelManager.channels[handle] del ChannelManager.results[handle] del ChannelManager.sessions[handle] except KeyError: pass @staticmethod def status(handle: int) -> str: """Check if a channel is open.""" return "open" if handle in ChannelManager.channels else "closed" @staticmethod def send( handle: int, session: Optional[int], expr: str, reply_id: Optional[int] = None, returns: bool = True, ) -> bool: """Send a command request or reply on a channel.""" try: ch = ChannelManager.channels[handle] except KeyError: return False if reply_id is None and session is not None: if ChannelManager.sessions.get(handle, None) == session: return True ChannelManager.sessions[handle] = session msg_id = reply_id if reply_id is not None else next(ChannelManager.msg_id) ch.sendall(_to_jsonl([msg_id, expr])) if returns: ChannelManager.results[handle] = ChannelManager.pool.submit( ChannelManager._recv, ChannelManager.channels[handle], ) return True @staticmethod def poll(handle: int) -> Optional[str]: """Wait for a response on a channel.""" try: return ChannelManager.results[handle].result(timeout=0) except futures.TimeoutError: return None @staticmethod def _recv(channel: socket.socket) -> Optional[str]: """Wait for a response on a channel.""" data = [] while True: try: data.append(channel.recv(4096).decode("utf-8")) # NOTE: Some older Vims can't convert expressions with None to # Vim values so just return a string res = "".join(data) _ = json.loads(res) return res except json.JSONDecodeError: pass except (KeyError, ConnectionError): return None # Searching for Coq Definitions # # TODO: could search more intelligently by searching only within relevant # section/module, or sometimes by looking at the type (for constructors for # example, or record projections) def get_searches(tgt_type: str, tgt_name: str) -> List[str]: """Construct a search expression given an object type and name.""" auto_names = [ ("Constructor", "Inductive", "Build_(.*)", 1), ("Constant", "Inductive", "(.*)_(ind|rect?)", 1), ] type_to_vernac = { "Inductive": ["(Co)?Inductive", "Variant", "Class", "Record"], "Constant": [ "Definition", "Let", "(Co)?Fixpoint", "Function", "Instance", "Theorem", "Lemma", "Remark", "Fact", "Corollary", "Proposition", "Example", "Parameters?", "Axioms?", "Conjectures?", ], "Notation": ["Notation"], "Variable": ["Variables?", "Hypothes[ie]s", "Context"], "Ltac": ["Ltac"], "Module": ["Module"], "Module Type": ["Module Type"], } # Look for some implicitly generated names search_names = [tgt_name] search_types = [tgt_type] for from_type, to_type, pat, grp in auto_names: if tgt_type == from_type: match = re.match(pat, tgt_name) if match is not None: search_names.append(match.group(grp)) search_types.append(to_type) search_name = "|".join(search_names) # What Vernacular command to look for search_vernac = "|".join( vernac for typ in search_types for vernac in type_to_vernac.get(typ, []) ) return [ rf"<({search_vernac})>\s*\zs<({search_name})>", rf"<({search_name})>", ] # Finding Start and End of Coq Chunks # def _pos_from_offset(col: int, msg: bytes, offset: int) -> Tuple[int, int]: """Calculate the line and column of a given offset.""" msg = msg[:offset] lines = msg.split(b"\n") line = len(lines) - 1 col = len(lines[-1]) + (col if line == 0 else 0) return (line, col) def _between( buf: Sequence[bytes], start: Tuple[int, int], end: Tuple[int, int], ) -> bytes: """Return the text between a given start and end point (inclusive).""" sline, scol = start eline, ecol = end lines: List[bytes] = [] for idx, line in enumerate(buf[sline : eline + 1]): lcol = scol if idx == 0 else 0 rcol = ecol + 1 if idx == eline - sline else len(line) lines.append(line[lcol:rcol]) return b"\n".join(lines) def _get_message_range( lines: Sequence[bytes], after: Tuple[int, int], ) -> Mapping[str, Tuple[int, int]]: """Return the next sentence to send after a given point.""" end_pos = _find_next_sentence(lines, *after) return {"start": after, "stop": end_pos} def _find_next_sentence( lines: Sequence[bytes], sline: int, scol: int, ) -> Tuple[int, int]: """Find the next sentence to send to Coq.""" braces = {ord(c) for c in "{}"} bullets = {ord(c) for c in "-+*"} line, col = (sline, scol) while True: # Skip leading whitespace for line in range(sline, len(lines)): first_line = lines[line][col:].lstrip() if first_line.rstrip() != b"": col += len(lines[line][col:]) - len(first_line) break col = 0 else: # break not reached, nothing left in the buffer but whitespace raise NoDotError() # Skip leading comments if first_line.startswith(b"(*"): com_end = _skip_comment(lines, line, col) if com_end is None: raise UnmatchedError("(*", (line, col)) sline, col = com_end # Skip leading attributes elif first_line.startswith(b"#["): attr_end = _skip_attribute(lines, line, col) if attr_end is None: raise UnmatchedError("#[", (line, col)) sline, col = attr_end else: break # Check if the first character of the sentence is a bullet if first_line[0] in braces | bullets: # '-', '+', '*' can be repeated for c in first_line[1:]: if c in bullets and c == first_line[0]: col += 1 else: break return (line, col) # Check if this is a bracketed goal selector if _char_isdigit(first_line[0]): state = "digit" selcol = col selline = line max_line = len(lines) while selline < max_line: if selcol >= len(lines[selline]): selcol = 0 selline += 1 continue c = lines[selline][selcol] if state == "digit" and _char_isdigit(c): selcol += 1 elif state == "digit" and _char_isspace(c): state = "beforecolon" selcol += 1 elif state == "digit" and c == ord(":"): state = "aftercolon" selcol += 1 elif state == "beforecolon" and _char_isspace(c): selcol += 1 elif state == "beforecolon" and c == ord(":"): state = "aftercolon" selcol += 1 elif state == "aftercolon" and _char_isspace(c): selcol += 1 elif state == "aftercolon" and c == ord("{"): return (selline, selcol) else: break # Otherwise, find an ending '.' return _find_dot_after(lines, line, col) def _find_dot_after(lines: Sequence[bytes], sline: int, scol: int) -> Tuple[int, int]: """Find the next '.' after a given point.""" max_line = len(lines) while sline < max_line: line = lines[sline][scol:] dot_pos = line.find(b".") com_pos = line.find(b"(*") str_pos = line.find(b'"') elpi_pos = line.find(b"lp:{{") first_pos = dot_pos for p in (com_pos, str_pos, elpi_pos): if first_pos == -1 or (0 <= p < first_pos): first_pos = p if first_pos == -1: # Nothing on this line sline += 1 scol = 0 elif first_pos == com_pos: # We see a comment opening before the next '.' com_end = _skip_comment(lines, sline, scol + com_pos) if com_end is None: raise UnmatchedError("(*", (sline, scol + com_pos)) sline, scol = com_end elif first_pos == str_pos: # We see a string starting before the next '.' str_end = _skip_str(lines, sline, scol + str_pos) if str_end is None: raise UnmatchedError('"', (sline, scol + str_pos)) sline, scol = str_end elif first_pos == elpi_pos: lp_end = _skip_elpi(lines, sline, scol + elpi_pos) if lp_end is None: raise UnmatchedError("lp:{{", (sline, scol + elpi_pos)) sline, scol = lp_end elif line[dot_pos : dot_pos + 2].rstrip() == b".": # Don't stop for '.' used in qualified name or for '..' return (sline, scol + dot_pos) elif line[dot_pos : dot_pos + 3] == b"...": # But do allow '...' return (sline, scol + dot_pos + 2) elif line[dot_pos : dot_pos + 2] == b"..": # Skip second '.' scol += dot_pos + 2 else: scol += dot_pos + 1 raise NoDotError() def _skip_str( lines: Sequence[bytes], sline: int, scol: int, ) -> Optional[Tuple[int, int]]: """Skip the next block contained in " ".""" return _skip_block(lines, sline, scol, b'"', b'"') def _skip_comment( lines: Sequence[bytes], sline: int, scol: int, ) -> Optional[Tuple[int, int]]: """Skip the next block contained in (* *).""" return _skip_block(lines, sline, scol, b"(*", b"*)") # In an elpi antiquotation lp:{{ }} we currently ignore strings "" and comments % # For example the lp:{{ }} may end in the middle of a string "}}" or a comment % }} # which is not ideal, but intentional to agree with the current Coq parser # https://github.com/coq/coq/blob/f2bf445b8f4f5241ebdc348b69961041b4e57883/parsing/cLexer.ml#L542 # See also this discussion: https://github.com/whonore/Coqtail/pull/278#discussion_r841927125 def _skip_elpi( lines: Sequence[bytes], sline: int, scol: int, ) -> Optional[Tuple[int, int]]: """Skip the next block contained in lp:{{ }}.""" return _skip_block(lines, sline, scol, b"lp:{{", b"}}", {b"{{": _skip_br2}) def _skip_br2( lines: Sequence[bytes], sline: int, scol: int, ) -> Optional[Tuple[int, int]]: """Skip the next block contained in {{ }}.""" return _skip_block(lines, sline, scol, b"{{", b"}}") def _skip_attribute( lines: Sequence[bytes], sline: int, scol: int, ) -> Optional[Tuple[int, int]]: """Skip the next block contained in #[ ].""" return _skip_block(lines, sline, scol, b"#[", b"]", {b'"': _skip_str}) def _skip_block( lines: Sequence[bytes], sline: int, scol: int, sstr: bytes, estr: bytes, skips: Optional[Mapping[bytes, SkipFun]] = None, ) -> Optional[Tuple[int, int]]: """A generic function to skip the next block contained in sstr estr.""" assert lines[sline].startswith(sstr, scol) nesting = 1 max_line = len(lines) scol += len(sstr) if skips is None: skips = {} while nesting > 0: if sline >= max_line: return None line = lines[sline] blk_end = line.find(estr, scol) blk_end = blk_end if blk_end != -1 else None if sstr != estr: blk_start = line.find(sstr, scol, blk_end) blk_start = blk_start if blk_start != -1 else None else: blk_start = None assert blk_start is None or blk_end is None or blk_start < blk_end # Look for contained blocks to skip skip_stop = blk_start if blk_start is not None else blk_end skip_starts = [(line.find(skip, scol, skip_stop), skip) for skip in skips] skip_starts = [(start, skip) for start, skip in skip_starts if start != -1] skip_start, skip = min(skip_starts, default=(None, None)) if skip is not None and skip_start is not None: skip_end = skips[skip](lines, sline, skip_start) if skip_end is None: return None sline, scol = skip_end continue if blk_end is not None and blk_start is None: # Found an end and no new start scol = blk_end + len(estr) nesting -= 1 elif blk_start is not None: # Found a new start scol = blk_start + len(sstr) nesting += 1 else: # Nothing on this line sline += 1 scol = 0 return (sline, scol) # Region Highlighting # class Matcher: """Construct Vim regexes to pass to 'matchadd()' for an arbitrary region.""" class _Matcher: """Construct regexes for a row or column.""" def __getitem__(self, key: Tuple[Union[int, slice], str]) -> str: """Construct the regex.""" match_range, match_type = key match = [] if isinstance(match_range, slice): if match_range.start is not None and match_range.start > 1: match.append(rf"\%>{match_range.start - 1}{match_type}") if match_range.stop is not None: match.append(rf"\%<{match_range.stop}{match_type}") else: match.append(rf"\%{match_range}{match_type}") return "".join(match) def __init__(self) -> None: """Initialize the row/column matcher.""" self._matcher = Matcher._Matcher() def __getitem__(self, key: Tuple[slice, slice]) -> str: """Construct the regex. 'key' is [line-start : line-end, col-start : col-end] where positions are 0-indexed. Ranges are inclusive on the left and exclusive on the right. """ lines, cols = map(Matcher.shift_slice, key) assert lines.stop is not None if lines.start == lines.stop - 1: return self._matcher[lines.start, "l"] + self._matcher[cols, "c"] return r"\|".join( x for x in ( # First line self._matcher[lines.start, "l"] + self._matcher[cols.start :, "c"], # Middle lines ( self._matcher[lines.start + 1 : lines.stop - 1, "l"] + self._matcher[:, "c"] if lines.start + 1 < lines.stop - 1 else "" ), # Last line self._matcher[lines.stop - 1, "l"] + self._matcher[: cols.stop, "c"], ) if x != "" ) @staticmethod def shift_slice(s: slice) -> slice: """Shift a 0-indexed to 1-indexed slice.""" return slice( s.start + 1 if s.start is not None else 1, s.stop + 1 if s.stop is not None else None, ) matcher = Matcher() # Misc # def _strip_comments(msg: bytes) -> Tuple[bytes, List[Tuple[int, int]]]: """Replace all comments in 'msg' with whitespace.""" # pylint: disable=no-else-break # NOTE: Coqtop will ignore comments, but it makes it easier to inspect # commands in Coqtail (e.g. options in coqtop.do_option) if we remove them. nocom = [] com_pos = [] # Remember comment offset and length off = 0 nesting = 0 while msg != b"": start = msg.find(b"(*") end = msg.find(b"*)") if start == -1 and (end == -1 or (end != -1 and nesting == 0)): # No comments left nocom.append(msg) break elif start != -1 and (start < end or end == -1): # New nested comment if nesting == 0: nocom.append(msg[:start]) nocom.append(b" " * 2) # Replace '(*' com_pos.append((off + start, 0)) else: # Replace everything up to and including nested comment start. nocom.append(re.sub(rb"\S", b" ", msg[: start + 2])) msg = msg[start + 2 :] # Skip '(*' off += start + 2 nesting += 1 elif end != -1 and (end < start or start == -1): # End of a comment # Replace everything up to and including comment end. nocom.append(re.sub(rb"\S", b" ", msg[: end + 2])) msg = msg[end + 2 :] off += end + 2 nesting -= 1 if nesting == 0: com_pos[-1] = (com_pos[-1][0], off - com_pos[-1][0]) return b"".join(nocom), com_pos def _find_opaque_proof_end( buffer: Sequence[bytes], ranges: Iterable[Mapping[str, Tuple[int, int]]], ) -> Optional[Mapping[str, Tuple[int, int]]]: """ Find the end of the current proof to check if it's opaque. A proof that contains a non-opaque nested proof is considered non-opaque. A proof without an ending is also considered non-opaque. """ pdepth = 1 for range_ in ranges: message, _ = _strip_comments(_between(buffer, range_["start"], range_["stop"])) pstart = PROOF_START_PAT.match(message) pend = PROOF_END_PAT.match(message) if pstart is not None: pdepth += 1 elif pend is not None: pdepth -= 1 if pdepth == 0 and pend.group(1) in OPAQUE_PROOF_ENDS: # Found a non-nested opaque end. return _shrink_range_to_match(range_, pend.group(), pend.start(1)) if pend.group(1) not in OPAQUE_PROOF_ENDS: # Found a non-opaque end. return None if pdepth == 0: break return None def _shrink_range_to_match( range_: Mapping[str, Tuple[int, int]], match: bytes, match_off: int, ) -> Mapping[str, Tuple[int, int]]: """Shrink a sentence range to begin at the start of a given match.""" nline_breaks = match.count(b"\n") sline = range_["start"][0] + nline_breaks # Offset the match start by the initial column if there are no line breaks, # else discount everything before the last line break. scol = match_off + ( range_["start"][1] if nline_breaks == 0 else -(match.rindex(b"\n") + 1) ) return {"start": (sline, scol), "stop": range_["stop"]} def _find_diff( x: Iterable[T], y: Iterable[T], stop: Optional[int] = None, ) -> Optional[int]: """Locate the first differing element in 'x' and 'y' up to 'stop' (exclusive). """ seq: Iterator[Tuple[int, Tuple[T, T]]] = enumerate(zip_longest(x, y)) if stop is not None: seq = islice(seq, stop) return next((i for i, vs in seq if vs[0] != vs[1]), None) def _diff_lines( old: Sequence[bytes], new: Sequence[bytes], stop: Tuple[int, int], ) -> Optional[Tuple[int, int]]: """Locate the first differing position in 'old' and 'new' lines of text up to 'stop' (exclusive). """ sline, scol = stop linediff = _find_diff(old, new, sline + 1) if linediff is None: return None try: coldiff = _find_diff( old[linediff], new[linediff], scol if linediff == sline else None, ) except IndexError: linediff = len(new) - 1 coldiff = len(new[-1]) if coldiff is None: return None return (linediff, coldiff) def _char_isdigit(c: int) -> bool: return ord("0") <= c <= ord("9") def _char_isspace(c: int) -> bool: return c in b" \t\n\r\x0b\f" def _to_jsonl(obj: Any) -> bytes: return (json.dumps(obj) + "\n").encode("utf-8") ))entry(name coqtop.pynode(typeregularcontentsša# -*- coding: utf8 -*- # Author: Wolf Honore """Coqtop interface with functions to send commands and parse responses.""" import datetime import logging import signal import subprocess import threading import time from concurrent import futures from contextlib import contextmanager from queue import Empty, Queue from tempfile import NamedTemporaryFile from typing import ( IO, TYPE_CHECKING, Any, Generator, Iterable, Iterator, List, Mapping, Optional, Tuple, Union, ) from xmlInterface import ( STDERR_ERR, TIMEOUT_ERR, Err, FindCoqtopError, GoalMode, Goals, Ok, Result, XMLInterface, XMLInterfaceBase, partition_warnings, prettyxml, ) if TYPE_CHECKING: from typing_extensions import TypedDict BytesQueue = Queue[bytes] CoqtopProcess = subprocess.Popen[bytes] VersionInfo = TypedDict( "VersionInfo", { "version": Tuple[int, int, int], "str_version": str, "latest": Optional[str], }, ) else: BytesQueue = Queue CoqtopProcess = subprocess.Popen VersionInfo = Mapping[str, Any] def join_not_empty(msgs: Iterable[str], joiner: str = "\n\n") -> str: """Concatenate non-empty messages.""" return joiner.join(msg for msg in msgs if msg != "") class CoqtopError(Exception): """An exception for when Coqtop stops unexpectedly.""" class Coqtop: """Provide an interface to the background Coqtop process.""" def __init__(self) -> None: """Initialize Coqtop state. coqtop - The Coqtop process states - A stack of previous state_ids (grows to the right) state_id - The current (tip) state_id root_state - The starting state_id out_q - A thread-safe queue of data read from Coqtop err_q - A thread-safe queue of error messages read from Coqtop xml - The XML interface for the given version """ self.coqtop: Optional[CoqtopProcess] = None self.xml: Optional[XMLInterfaceBase] = None self.states: List[int] = [] self.state_id = -1 self.root_state = -1 self.out_q: BytesQueue = Queue() self.err_q: BytesQueue = Queue() self.stopping = False # Debugging self.log: Optional[IO[str]] = None self.handler: logging.Handler = logging.NullHandler() self.logger = logging.getLogger(str(id(self))) self.logger.addHandler(self.handler) self.logger.setLevel(logging.INFO) # Coqtop Interface # def start( self, coq_path: Optional[str], coq_prog: Optional[str], filename: str, args: Iterable[str], timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[Union[VersionInfo, str], str]: """Launch the Coqtop process.""" assert self.coqtop is None try: self.logger.debug("start") self.xml, latest = XMLInterface(coq_path, coq_prog) launch = self.xml.launch(filename, args) self.logger.debug(launch) self.coqtop = subprocess.Popen( # pylint: disable=consider-using-with launch, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE, bufsize=0, ) # Ensure that Coqtop spawned correctly try: self.coqtop.wait(timeout=0.1) assert self.coqtop.stderr is not None return self.coqtop.stderr.read().decode("utf8"), "" except subprocess.TimeoutExpired: pass # Spawn threads to monitor Coqtop's stdout and stderr for buf, stream in ( (self.out_q, self.coqtop.stdout), (self.err_q, self.coqtop.stderr), ): threading.Thread( target=self.capture_out, args=(buf, stream), daemon=True, ).start() threading.Thread(target=self.capture_dead, daemon=True).start() # Initialize Coqtop response, err = self.call( self.xml.init(), timeout=timeout, stderr_is_warning=stderr_is_warning, ) if isinstance(response, Err): return response.msg, err self.root_state = response.val self.state_id = response.val return ( { "version": self.xml.version, "str_version": self.xml.str_version, "latest": latest, }, err, ) except (OSError, FindCoqtopError) as e: # Failed to launch or find Coqtop self.coqtop = None return str(e), "" def stop(self) -> None: """End the Coqtop process.""" if self.coqtop is not None: self.logger.debug("stop") self.stopping = True try: # Try to terminate Coqtop cleanly # TODO: use Quit call self.coqtop.terminate() self.coqtop.communicate() except (OSError, ValueError, AttributeError): try: # Force Coqtop to stop self.coqtop.kill() except (OSError, AttributeError): pass self.coqtop = None # Close debugging log try: self.handler.flush() self.handler.close() except ValueError: pass if self.log is not None and not self.log.closed: self.log.close() def advance( self, cmd: str, encoding: str = "utf-8", timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Tuple[int, int]], str]: """Advance Coqtop by sending 'cmd'.""" assert self.xml is not None self.logger.debug("advance: %s", cmd) response, err1 = self.call( self.xml.add(cmd, self.state_id, encoding=encoding), timeout=timeout, stderr_is_warning=stderr_is_warning, ) if isinstance(response, Err): return False, response.msg, response.loc, err1 # In addition to sending 'cmd', also check status in order to force it # to be evaluated status, err2 = self.call( self.xml.status(encoding=encoding), timeout=timeout, stderr_is_warning=stderr_is_warning, ) # Combine messages msgs = join_not_empty((response.msg, response.val["res_msg"], status.msg)) err = err1 + err2 if isinstance(status, Err): # Reset state id to before the error self.call( self.xml.edit_at(self.state_id, 1), stderr_is_warning=stderr_is_warning, ) return False, msgs, status.loc, err self.states.append(self.state_id) self.state_id = response.val["state_id"] return True, msgs, None, err def rewind( self, steps: int = 1, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[int], str]: """Go back 'steps' states.""" assert self.xml is not None self.logger.debug("rewind: %d", steps) if steps > len(self.states): self.state_id = self.root_state self.states = [] steps = len(self.states) else: # In 8.4 query and option commands will be recorded with # state_id = -1. Need to count them and reduce number of steps to # rewind so Coqtop doesn't go too far back fake_steps = sum(s == -1 for s in self.states[-steps:]) if self.states[-steps] != -1: self.state_id = self.states[-steps] else: self.state_id = 0 self.states = self.states[:-steps] steps -= fake_steps response, err = self.call( self.xml.edit_at(self.state_id, steps), stderr_is_warning=stderr_is_warning, ) return ( isinstance(response, Ok), response.msg, response.val if isinstance(response, Ok) else None, err, ) def query( self, cmd: str, in_script: bool, encoding: str = "utf-8", timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Tuple[int, int]], str]: """Query Coqtop with 'cmd'.""" assert self.xml is not None self.logger.debug("query: %s", cmd) response, err = self.call( self.xml.query(cmd, self.state_id, encoding=encoding), timeout=timeout, stderr_is_warning=stderr_is_warning, ) if isinstance(response, Ok) and in_script: # If the query was called from within the script we need to record # the state id so rewinding will work properly. Since 8.4 uses # number of steps rather than state ids, record '-1' to indicate # that no rewind should actually be done if self.xml.version >= (8, 5, 0): self.states.append(self.state_id) else: self.states.append(-1) return ( isinstance(response, Ok), response.msg, None if isinstance(response, Ok) else response.loc, err, ) def goals( self, timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Goals], str]: """Get the current set of hypotheses and goals.""" assert self.xml is not None self.logger.debug("goals") # Use Subgoals if available, otherwise fall back to Goal if hasattr(self.xml, "subgoal"): return self.subgoals(timeout=timeout, stderr_is_warning=stderr_is_warning) response, err = self.call( self.xml.goal(), timeout=timeout, stderr_is_warning=stderr_is_warning, ) return ( isinstance(response, Ok), response.msg, response.val if isinstance(response, Ok) else None, err, ) def subgoals( self, timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Goals], str]: """Get the current set of hypotheses and goals.""" assert self.xml is not None # Get the current proof state, but only include focused # goals in the goal list. response_main, err_main = self.call( self.xml.subgoal( # type: ignore GoalMode.FULL, fg=True, bg=False, shelved=False, given_up=False, ), timeout=timeout, stderr_is_warning=stderr_is_warning, ) if isinstance(response_main, Err): return (False, response_main.msg, None, err_main) # If success but we didn't get a CoqGoals, then there's # no proof in progress. We can return early. if response_main.val is None: # If the request was success but it returned None, then # we're not in a proof. No need to run the second query. return (True, response_main.msg, None, err_main) # NOTE: Subgoals ignores `gf_flag = "short"` if proof diffs are # enabled. # See: https://github.com/coq/coq/issues/16564 with self.suppress_diffs(stderr_is_warning=stderr_is_warning): # Get the short version of other goals (no hypotheses) response_extra, err_extra = self.call( self.xml.subgoal( # type: ignore GoalMode.SHORT, fg=False, bg=True, shelved=True, given_up=True, ), timeout=timeout, stderr_is_warning=stderr_is_warning, ) # Combine messages msgs = join_not_empty(response_main.msg, response_extra.msg) errs = err_main + err_extra if isinstance(response_extra, Err): return (False, msgs, None, errs) assert response_extra.val is not None, "proof state changed unexpectedly?" # Merge goals goals = Goals( response_main.val.fg, response_extra.val.bg, response_extra.val.shelved, response_extra.val.given_up, ) return (True, msgs, goals, errs) def do_option( self, cmd: str, in_script: bool, encoding: str = "utf-8", timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Tuple[int, int]], str]: """Set or get an option's value.""" assert self.xml is not None self.logger.debug("do_option: %s", cmd) vals, opt = self.xml.parse_option(cmd) option_ok = True if vals is None: response, err = self.call( self.xml.get_options(encoding=encoding), timeout=timeout, stderr_is_warning=stderr_is_warning, ) if isinstance(response, Ok): try: ret = next( ( f"{desc}: {val}" for name, desc, val in response.val if name == opt ) ) except StopIteration: ret = "Invalid option name" option_ok = False else: errs = [] for val in vals: response, err = self.call( self.xml.set_options(opt, val, encoding=encoding), timeout=timeout, stderr_is_warning=stderr_is_warning, ) ret = response.msg # `set_options()` returns nothing on success option_ok = option_ok and ret == "" errs.append(err) if isinstance(response, Ok): break err = "".join(errs) if in_script and isinstance(response, Ok) and option_ok: # Hack to associate setting an option with a new state id by # executing a noop so it works correctly with rewinding success, _, _, _ = self.advance( self.xml.noop, encoding=encoding, stderr_is_warning=stderr_is_warning, ) assert success elif in_script and not option_ok: # Fall back to using `advance()` in case the best-effort attempt at # using `SetOptions` only failed because the option's value doesn't # follow the usual pattern (e.g., `Firstorder Solver`) self.logger.warning("Failed to handle %s with Get/SetOptions", cmd) return self.advance( cmd, encoding=encoding, timeout=timeout, stderr_is_warning=stderr_is_warning, ) return ( isinstance(response, Ok), ret if isinstance(response, Ok) else response.msg, None if isinstance(response, Ok) else response.loc, err, ) def dispatch( self, cmd: str, cmd_no_comment: Optional[str] = None, in_script: bool = True, encoding: str = "utf-8", timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[bool, str, Optional[Tuple[int, int]], str]: """Decide whether 'cmd' is setting/getting an option, a query, or a regular command. """ # pylint: disable=no-else-return assert self.xml is not None if cmd_no_comment is None: cmd_no_comment = cmd if self.xml.is_option(cmd_no_comment): return self.do_option( cmd_no_comment, in_script, encoding=encoding, timeout=timeout, stderr_is_warning=stderr_is_warning, ) elif self.xml.is_query(cmd_no_comment): return self.query( cmd, in_script, encoding=encoding, timeout=timeout, stderr_is_warning=stderr_is_warning, ) elif in_script: return self.advance( cmd, encoding=encoding, timeout=timeout, stderr_is_warning=stderr_is_warning, ) else: return True, "Command only allowed in script.", None, "" @contextmanager def suppress_diffs( self, timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Generator[None, None, None]: """Temporarily disable proof diffs.""" # Check if diffs are enabled expect_prefix = "Diffs: Some(val=" ok, response, _, err = self.do_option( "Test Diffs", in_script=False, timeout=timeout, stderr_is_warning=stderr_is_warning, ) if ok and response.startswith(expect_prefix): # TODO: Make a cleaner way of reading an option diffs = response[len(expect_prefix) : -1].strip("'") else: # Failures are just logged because there's not much else that can # be done from here. self.logger.warning("Failed to read Diffs option: %s", err) diffs = "off" # Disable if necessary if diffs != "off": ok, _, _, err = self.do_option( 'Set Diffs "off"', in_script=False, timeout=timeout, stderr_is_warning=stderr_is_warning, ) if not ok: self.logger.warning("Failed to disable Diffs option: %s", err) yield None # Re-enable if necessary if diffs != "off": ok, _, _, err = self.do_option( f'Set Diffs "{diffs}"', in_script=False, timeout=timeout, stderr_is_warning=stderr_is_warning, ) if not ok: self.logger.warning("Failed to re-enable Diffs option: %s", err) # Interacting with Coqtop # def call( self, cmdtype_msg: Tuple[str, Optional[bytes]], timeout: Optional[int] = None, stderr_is_warning: bool = False, ) -> Tuple[Result, str]: """Send 'msg' to the Coqtop process and wait for the response.""" assert self.xml is not None # Check if Coqtop has stopped if not self.running(): raise CoqtopError("Coqtop is not running.") # Throw away any unread messages self.empty_out() # 'msg' can be None if a command does not exist for a particular # version and is being faked. # NOTE: It is important that the '_standardize' function being called # does not depend on the value it is passed since it is None cmd, msg = cmdtype_msg if msg is None: return self.xml.standardize(cmd, Ok(None)), self.collect_err() # Don't bother doing prettyxml if debugging isn't on if self.logger.isEnabledFor(logging.DEBUG): self.logger.debug(prettyxml(msg)) self.send_cmd(msg) with futures.ThreadPoolExecutor(1) as pool: try: timeout = None if timeout == 0 else timeout response, err = pool.submit( lambda: self.get_answer(stderr_is_warning) ).result(timeout) except futures.TimeoutError: self.interrupt() response, err = TIMEOUT_ERR, "" return self.xml.standardize(cmd, response), err def get_answer(self, stderr_is_warning: bool = False) -> Tuple[Result, str]: """Read from 'out_q' and wait until a full response is received.""" assert self.xml is not None data = [] poll_sec = 1 while True: # Abort if an error is printed to stderr, but ignore warnings. # NOTE: If `warnings_wf` is False because this version of Coq does # not follow the pattern expected by `partition_warnings` then # pretend everything is a warning and hope for the best. # The `stderr_is_warning` option also causes any any message # on stderr to be treated as a warning. err = self.collect_err() if ( not stderr_is_warning and self.xml.warnings_wf and partition_warnings(err)[1] != "" ): return STDERR_ERR, err try: data.append(self.out_q.get(timeout=poll_sec)) except Empty: continue xml = b"".join(data) if not self.xml.worth_parsing(xml): continue response = self.xml.raw_response(xml) if response is None: continue # Don't bother doing prettyxml if debugging isn't on if self.logger.isEnabledFor(logging.DEBUG): self.logger.debug(prettyxml(b"" + xml + b"")) return response, err @staticmethod def drain_queue(q: BytesQueue) -> Iterator[bytes]: """Yield data from 'q' until it is empty.""" while not q.empty(): try: yield q.get_nowait() except Empty: return def empty_out(self) -> None: """Pop data until 'out_q' is empty.""" for _ in Coqtop.drain_queue(self.out_q): pass def collect_err(self) -> str: """Pop and concatenate everything in 'err_q'.""" err = b"".join(Coqtop.drain_queue(self.err_q)).decode("utf-8") if err != "": self.logger.debug(err) return err def capture_out(self, buffer: BytesQueue, stream: IO[bytes]) -> None: """Continually read data from 'stream' into 'buffer'.""" while not self.stopping: try: buffer.put(stream.read(0x10000)) except (AttributeError, OSError, ValueError): # Coqtop died return def capture_dead(self) -> None: """Continually check if Coqtop has died.""" while self.running(): time.sleep(1) self.stop() def send_cmd(self, cmd: bytes) -> None: """Write to Coqtop's stdin.""" if self.coqtop is None: raise CoqtopError("coqtop must not be None in send_cmd()") if self.coqtop.stdin is None: raise CoqtopError("coqtop stdin must not be None in send_cmd()") self.coqtop.stdin.write(cmd) self.coqtop.stdin.flush() def interrupt(self) -> None: """Send a SIGINT signal to Coqtop.""" if self.coqtop is None: raise CoqtopError("Coqtop is not running.") self.coqtop.send_signal(signal.SIGINT) # Current State # def running(self) -> bool: """Check if Coqtop has already been started.""" return self.coqtop is not None and self.coqtop.poll() is None # Debugging # def toggle_debug(self) -> Optional[str]: """Enable or disable logging of debug messages.""" self.logger.removeHandler(self.handler) self.handler.flush() self.handler.close() if self.log is None: # Create unique log file fmt = logging.Formatter("%(asctime)s: %(message)s") self.log = NamedTemporaryFile( # pylint: disable=consider-using-with mode="w", encoding="utf-8", prefix=f"coqtop_{datetime.datetime.now().strftime('%y%m%d_%H%M%S')}_", delete=False, ) self.handler = logging.StreamHandler(self.log) self.handler.setFormatter(fmt) self.logger.addHandler(self.handler) self.logger.setLevel(logging.DEBUG) else: # Clean up old logging self.log.close() # Set to null logging self.log = None self.handler = logging.NullHandler() self.logger.addHandler(self.handler) self.logger.setLevel(logging.CRITICAL) return self.log.name if self.log is not None else None ))entry(namexmlInterface.pynode(typeregularcontents˜ż# -*- coding: utf8 -*- # Author: Wolf Honore """Classes to handle differences in the Coqtop XML interface across versions and provide a uniform interface. https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md """ # xml.dom.minidom only needed for pretty printing. import re import subprocess import xml.etree.ElementTree as ET from abc import ABCMeta, abstractmethod from enum import Enum from pathlib import Path from shutil import which from typing import ( Any, Callable, Container, Dict, Iterable, Iterator, List, NamedTuple, Optional, Sequence, Tuple, Union, cast, ) from xml.dom.minidom import parseString from xml.parsers.expat import ExpatError, errors PPTag = str TaggedToken = Tuple[str, Optional[PPTag]] Goal = NamedTuple( "Goal", [ ("hyp", Sequence[Union[str, Sequence[TaggedToken]]]), ("ccl", Union[str, Sequence[TaggedToken]]), ("name", Optional[str]), ], ) Goals = NamedTuple( "Goals", [ ("fg", List[Goal]), ("bg", List[List[Goal]]), ("shelved", List[Goal]), ("given_up", List[Goal]), ], ) class GoalMode(Enum): """Control the information returned by the Subgoals command.""" # Get the goal and hypotheses FULL = "full" # Get only the goal SHORT = "short" WARNING_RE = re.compile("^(Warning:[^]]+])$", flags=re.MULTILINE) class FindCoqtopError(Exception): """An exception for when a coqtop executable could not be found.""" # Coqtop Response Types # class Ok: """A response representing success.""" def __init__(self, val: Any, msg: str = "") -> None: """Initialize values.""" self.val = val self.msg = msg class Err: """A response representing failure.""" def __init__(self, msg: str, loc: Tuple[int, int] = (-1, -1)) -> None: """Initialize values.""" self.msg = msg self.loc = loc Result = Union[Ok, Err] # The error in case of a timeout TIMEOUT_ERR = Err( "Coq timed out. You can change the timeout with ct and try again." ) # The error in case of a message on stderr STDERR_ERR = Err( "Coqtail received an unexpected error message on stderr. " "Please report at https://github.com/whonore/Coqtail/issues." "\n\n" "This can sometimes happen if the message is actually a warning, but is not " "formatted in a way that Coqtail recognizes. " "If you wish to ignore this error and try to proceed past it, set " "g:coqtail_treat_stderr_as_warning = 1." ) # Helpers # def unexpected(expected: Iterable[Any], got: Any) -> TypeError: """Return an exception with a message showing what was expected.""" expect = " or ".join(map(str, expected)) return TypeError(f"Expected {expect}, but got {str(got)}") CHARMAP = {b" ": b" ", b"'": b"'", b"(": b"(", b")": b")"} BAD_BYTE = errors.codes[errors.XML_ERROR_INVALID_TOKEN] # pylint: disable=no-member def _unescape(cmd: bytes) -> bytes: """Replace escaped characters with the unescaped version.""" for escape, unescape in CHARMAP.items(): cmd = cmd.replace(escape, unescape) return cmd def _escape_byte(data: bytes, line: int, col: int) -> bytes: """Escape an unprintable byte.""" lines = data.splitlines() bad = lines[line - 1][col] pre = lines[line - 1][:col] post = lines[line - 1][col + 1 :] lines[line - 1] = pre + f"\\x{bad:02x}".encode("utf-8") + post return b"\n".join(lines) def _parse_tagged_tokens( tags: Container[PPTag], xml: ET.Element, stack: Optional[List[PPTag]] = None, inner: bool = False, ) -> Iterator[Tuple[str, List[PPTag]]]: """Scrape an XML element into a stream of text tokens and stack of tags. Helper function to parse_tagged_tokens. Written to support richpp tags, and thus supports .start and .end tags used by Coqtop to highlight ranges that are not properly nested (i.e., ......... is allowed). This is somewhat documented here: https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md#highlighting-text Documentation neglects to mention the semantics of start. and end. tags that are not self-closing. Until we get clarification, we will interpret foobar as foobar and foobar as foobar. """ pop_after = None if stack is None: stack = [] # Check tag, see if we should modify stack if xml.tag.startswith("start."): _, _, tag = xml.tag.rpartition("start.") # assert(tag != "") if tag in tags: # start. tag: push onto stack stack.insert(0, tag) elif xml.tag.startswith("end."): _, _, tag = xml.tag.rpartition("end.") # assert(tag != "") if tag in tags: # end. tag: remove from stack (even if it's not at the top) pop_after = tag elif xml.tag in tags: # regular tag: push onto stack, but remember to pop it before xml.tail stack.insert(0, xml.tag) pop_after = xml.tag # Get text before first inner child if xml.text is not None: yield (xml.text, stack[:]) # Recurse on children, with modified stack for child in xml: yield from _parse_tagged_tokens(tags, child, stack, True) if pop_after is not None: stack.remove(pop_after) # Get trailing text up to start of next tag, unless this is the outermost tag if inner and xml.tail is not None: yield (xml.tail, stack[:]) def parse_tagged_tokens( tags: Container[PPTag], xml: ET.Element, ) -> Iterator[TaggedToken]: """Scrape an XML element into a stream of text tokens and accompanying tags. Written to support richpp markup. Only considers tags specified by the tags parameter. """ token_acc, last_tag = "", None # Recursive helper _parse_tagged_tokens gives us tag stacks for token, tag_list in _parse_tagged_tokens(tags, xml): # Take top tag from tag stack, if any top_tag = tag_list[0] if tag_list != [] else None if top_tag == last_tag: # Join tokens whose top tag is the same token_acc += token else: yield (token_acc, last_tag) token_acc, last_tag = token, top_tag yield (token_acc, last_tag) def join_tagged_tokens(tagged_tokens: Iterable[TaggedToken]) -> str: """Join tokens from tagged token stream. NOTE: forall xml tags, join_tagged_tokens(parse_tagged_token(tags, xml)) = "".join(xml.itertext()) """ return "".join(s for s, _ in tagged_tokens) def partition_warnings(stderr: str) -> Tuple[str, str]: """Partition Coq stderr messages into warnings and errors. Warnings are assumed to have the following form: Warning: message_with_newlines [warning_type]\n Everything else is treated as an error message. """ warns: List[str] = [] errs: List[str] = [] # Strip whitespace and drop empty strings for msg in filter(None, map(str.strip, WARNING_RE.split(stderr))): (warns if WARNING_RE.fullmatch(msg) else errs).append(msg) return "\n".join(warns), "\n".join(errs) # Debugging # def prettyxml(xml: bytes) -> str: """Pretty print XML for debugging.""" xml = _unescape(xml) # See `XMLInterfaceBase.raw_response`. err_pos = (-1, -1) while True: try: return parseString(xml).toprettyxml() except ExpatError as e: if e.code != BAD_BYTE or (e.lineno, e.offset) <= err_pos: raise e err_pos = (e.lineno, e.offset) xml = _escape_byte(xml, *err_pos) class XMLInterfaceBase(metaclass=ABCMeta): """Provide methods and types common to all XML interface versions.""" # Coqtop Types # sentinel = object() # Option Type Some = NamedTuple("Some", [("val", Any)]) CoqOption = Union[Some, None] # Union type Inl = NamedTuple("Inl", [("val", Any)]) Inr = NamedTuple("Inr", [("val", Any)]) CoqUnion = Union[Inl, Inr] # Types accepted by 'Set {option} {val}' OptionArg = Union[bool, int, str, Tuple[None, str]] def __init__( self, version: Tuple[int, int, int], str_version: str, coq_path: str, coq_prog: Optional[str], ) -> None: """Initialize maps for converting between XML and Python values.""" self.version = version self.str_version = str_version # Coqtop launch arguments self.coq_path = coq_path assert coq_prog is not None self.coq_prog = coq_prog self.launch_args = ["-ideslave"] # Valid query commands self.queries = [ "Search", "SearchAbout", "SearchPattern", "SearchRewrite", "Check", "Print", "About", "Locate", "Show", ] # Map from Python types to appropriate XML marshalling function self._to_py_funcs: Dict[str, Callable[[ET.Element], Any]] = { "unit": self._to_unit, "bool": self._to_bool, "int": self._to_int, "string": self._to_string, "list": self._to_list, "pair": self._to_pair, "option": self._to_option, "union": self._to_union, } # Inverse map self._of_py_funcs: Dict[str, Callable[[Any], ET.Element]] = { # Special case for tuple, must distinguish between 'unit' and # 'pair' by checking for '()' "tuple": lambda v: self._of_pair(v) if v else self._of_unit(v), "bool": self._of_bool, "int": self._of_int, "str": self._of_string, "list": self._of_list, "Some": self._of_option, "NoneType": self._of_option, "Inl": self._of_union, "Inr": self._of_union, } # Map from coqtop command to standardization function self._standardize_funcs: Dict[str, Callable[[Result], Result]] = {} # A command that can safely and quickly be executed just to get a new state id self.noop = "Check Prop." # A flag indicating whether warnings printed to stderr are formatted in # the manner expected by partition_warnings self.warnings_wf = False def launch(self, filename: str, args: Iterable[str]) -> Tuple[str, ...]: """The command to launch coqtop with the appropriate arguments.""" # Find the executable try: coqs = ( p for p in ( which(pre + self.coq_prog + ext, path=self.coq_path) for pre in ("", "coq-prover.") for ext in ("", ".opt") ) if p is not None ) coq = next(coqs) except StopIteration as e: path = "$PATH" if self.coq_path is None else self.coq_path raise FindCoqtopError( f"Could not find {self.coq_prog} in {path}. Perhaps you need " "to set g:coqtail_coq_path or g:coqtail_coq_prog." ) from e # Confirm the version matches version = parse_version(extract_version(coq)) if version != self.version: raise FindCoqtopError( f"{coq} version does not match version reported by coqc.\n" f"Expected: {self.version} Got: {version}" ) return ( (coq,) + tuple(self.launch_args) + self.topfile(filename, args) + tuple(args) ) @staticmethod def topfile(filename: str, args: Iterable[str]) -> Tuple[str, ...]: """The command to set the top-level module name.""" # pylint: disable=unused-argument # The arguments are only used in XMLInterface810 and greater. return () @staticmethod def valid_module(filename: str) -> bool: """Check if a file name is a valid module name.""" # Any string of word characters that doesn't start with a digit return re.fullmatch(r"(?=\D)\w+", Path(filename).stem) is not None # XML Parsing and Marshalling # def _to_unit(self, _xml: ET.Element) -> Tuple[()]: """Expect: """ return () def _of_unit(self, _val: Tuple[()]) -> ET.Element: """Expect: ()""" return self._build_xml("unit") def _to_bool(self, xml: ET.Element) -> bool: """Expect: """ # pylint: disable=no-else-return val = xml.get("val") if val == "true": return True elif val == "false": return False raise unexpected(("true", "false"), val) def _of_bool(self, val: bool) -> ET.Element: """Expect: True | False""" return self._build_xml("bool", str(val).lower()) def _to_int(self, xml: ET.Element) -> int: """Expect: int""" if xml.text is not None: return int(xml.text) raise unexpected((str,), None) def _of_int(self, val: int) -> ET.Element: """Expect: int""" return self._build_xml("int", text=str(val)) def _to_string(self, xml: ET.Element) -> str: """Expect: str""" return "".join(xml.itertext()) def _of_string(self, val: str) -> ET.Element: """Expect: str""" return self._build_xml("string", text=val) def _to_list(self, xml: ET.Element) -> List[Any]: """Expect: val val ...""" return [self._to_py(val) for val in xml] def _of_list(self, val: List[Any]) -> ET.Element: """Expect: [val, val, ...]""" return self._build_xml("list", children=val) def _to_pair(self, xml: ET.Element) -> Tuple[Any, Any]: """Expect: val1 val2""" return (self._to_py(xml[0]), self._to_py(xml[1])) def _of_pair(self, val: Tuple[Any, Any]) -> ET.Element: """Expect: (val1, val2)""" return self._build_xml("pair", children=[val[0], val[1]]) def _to_option(self, xml: ET.Element) -> "CoqOption": """Expect: |