tree-sitter / tree-sitter-agda Goto Github PK

View Code? Open in Web Editor NEW

32.0 7.0 15.0 31.13 MB

Agda grammar for tree-sitter

License: MIT License

Python 0.25% JavaScript 21.19% C++ 0.65% Yacc 75.36% Rust 1.89% Scheme 0.67%

tree-sitter context-free-grammar syntax-highlighting agda

tree-sitter-agda's Introduction

Agda Grammar for tree-sitter

Syntax highlighting and code folding done right (with context-free grammar, finally!)

How to contribute

documentation

Install dependencies:

npm install

To see if you have tree-sitter installed:

npx tree-sitter

To generate the parser:

npx tree-sitter generate

Run test to see if everything's okay:

npm test

You may wanna run this on the language-agda's side:

npm install
apm rebuild

tree-sitter-agda's People

Contributors

Stargazers

Watchers

Forkers

typesanitizer rwe isabella232 auscyber cursorless-dev flupe wenkokke varungandhi-src seanpm2001 cengelbart39 omentic lamiya1234 verhovsky panekj

tree-sitter-agda's Issues

Assertion failed: symbol < self->token_count (lib/src/language.c: ts_language_table_entry: 46)

This assertion fails whenever telescope asks nvim-treesitter to preview this file:
https://codeberg.org/foxy/extracting-programs-from-proofs/src/commit/b6fc6b8aa354ba169ba3d623aa98ccbb1162b3ef/Verona2024/Basics/Negation.agda
and neovim itself crashes. Whenever I am directly opening the file, this failure is apparently handled more gracefully, so I manage to see where treesitter stops parsing (empty line 26).

Implicit narrowing conversion might create trouble

queued_dedent_count has type uint32_t whereas buffer has type char*, so you'll wrap around for deeply indented code.

tree-sitter-agda/src/scanner.cc

Line 23 in 59cefa7

buffer[i++] = queued_dedent_count;

This line has a similar problem where uint16_t will get narrowed to char, so non-ASCII characters will be misrepresented.

tree-sitter-agda/src/scanner.cc

Line 29 in 59cefa7

buffer[i++] = *iter;

Maybe I'm grossly misunderstanding something -- the example in the Readme does show non-ASCII symbols and somehow it has been working fine?

No features appear

Using nvim-treesitter, no features appear, it's loaded correctly but the rust binding part or something doesnt declare the queries

Grammar failing with 0.15.3

Is this a bug?

(py364_32) D:\mcve\tree-sitter-agda>tree-sitter --version
tree-sitter 0.15.3 (4d4e4f3909358bb5abdc3c3de0640d1b4ff444fe)

(py364_32) D:\mcve\tree-sitter-agda>rm -rf src

(py364_32) D:\mcve\tree-sitter-agda>tree-sitter generate
Unresolved conflict for symbol sequence:

  atom  •  'integer_token1'  …

Possible interpretations:

  1:  (_atoms1  atom)  •  'integer_token1'  …
  2:  (lambda_clause_repeat1  atom)  •  'integer_token1'  …

Possible resolutions:

  1:  Add a conflict for these rules: `_application`

Agda filetype non-detected/non-existing

Whenever I open an .agda/.agda-lib file, the agda filetype is not detected, and hence the tree-sitter-agda (which is correctly installed) is not enabled on the buffer.

If I use :set filetype agda, the agda filetype seems to be never have been defined.

If I manually enable tree-sitter-agda via :TSEnable, nothing happens (no syntax highlighting).

All highlight seems broken

(After performing a fresh install of fresh Atom and the current language-agda plugin)
See all highlight in a strange new look. Reproducible in tree-sitter mode only.
Versions:

$ find .atom -name '*tree-sitter-agda*'
.atom/.apm/_prebuilds/ccb761-tree-sitter-agda-v1.1.0-electron-v64-linux-x64.tar.gz
.atom/packages/language-agda/grammars/tree-sitter-agda.cson
.atom/packages/language-agda/node_modules/tree-sitter-agda

$ rpm -aq atom
atom-1.39.0-0.1.x86_64

screenshot: https://gist.github.com/zraffer/f13cdf3da1fff8aa8f251542fc9ccea7#file-screenshot-png

Unicode symbols breaking the scanner

As in tree-sitter/tree-sitter#312

Failed to load a language-agda package grammar

In fresh install of Atom Beta 1.47 featuring Electron 5.0.
language-agda complains about tree-sitter build v47 vs. v70.
However it is v70 being actually loaded:
.atom/.apm/_prebuilds/c5e98d-tree-sitter-agda-v1.2.1-electron-v70-linux-x64.tar.gz

Atom: 1.47.0-beta0 x64
Electron: 5.0.13
OS: Ubuntu 20.04
Thrown From: language-agda package 1.2.0

Stack Trace

Failed to load a language-agda package grammar

At The module '/home/user/.atom/packages/language-agda/node_modules/tree-sitter-agda/build/Release/tree_sitter_agda_binding.node'
was compiled against a different Node.js version using
NODE_MODULE_VERSION 47. This version of Node.js requires
NODE_MODULE_VERSION 70. Please try re-compiling or re-installing
the module (for instance, using `npm rebuild` or `npm install`). in /home/user/.atom/packages/language-agda/grammars/tree-sitter-agda.cson

Error: The module '/home/user/.atom/packages/language-agda/node_modules/tree-sitter-agda/build/Release/tree_sitter_agda_binding.node'
was compiled against a different Node.js version using
NODE_MODULE_VERSION 47. This version of Node.js requires
NODE_MODULE_VERSION 70. Please try re-compiling or re-installing
the module (for instance, using `npm rebuild` or `npm install`).
    at process.func [as dlopen] (electron/js2c/asar.js:138:31)
    at Object.Module._extensions..node (internal/modules/cjs/loader.js:881:18)
    at Object.func [as .node] (electron/js2c/asar.js:138:31)
    at Module.load (internal/modules/cjs/loader.js:701:32)
    at tryModuleLoad (internal/modules/cjs/loader.js:633:12)
    at Function.Module._load (internal/modules/cjs/loader.js:625:3)
    at Module.require (/app.asar/static/index.js:72:46)
    at require (/usr/share/atom-beta/resources/app/static/<embedded>:11:146766)
    at /packages/language-agda/node_modules/tree-sitter-agda/index.js:2:20)
    at /packages/language-agda/node_modules/tree-sitter-agda/index.js:15:3)
    at Module.get_Module._compile (/usr/share/atom-beta/resources/app/static/<embedded>:11:147450)
    at Object.value [as .js] (/usr/share/atom-beta/resources/app/static/<embedded>:11:150998)
    at Module.load (internal/modules/cjs/loader.js:701:32)
    at tryModuleLoad (internal/modules/cjs/loader.js:633:12)
    at Function.Module._load (internal/modules/cjs/loader.js:625:3)
    at Module.require (/app.asar/static/index.js:72:46)
    at require (internal/modules/cjs/helpers.js:14:16)
    at customRequire (/usr/share/atom-beta/resources/app/static/<embedded>:1:695413)
    at new TreeSitterGrammar (/usr/share/atom-beta/resources/app/static/<embedded>:11:3113290)
    at GrammarRegistry.createGrammar (/usr/share/atom-beta/resources/app/static/<embedded>:11:360129)
    at /usr/share/atom-beta/resources/app/static/<embedded>:11:359970
    at /usr/share/atom-beta/resources/app/static/<embedded>:11:581856
    at FSReqCallback.readFileAfterClose [as oncomplete] (internal/fs/read_file_context.js:54:3)
  at /packages/language-agda/grammars/tree-sitter-agda.cson:1:1

Commands

     -0:30.2.0 window:toggle-menu-bar (div.welcome.is-guide)

Non-Core Packages

language-agda 1.2.0

npm install error on Win10

Hi,

I am trying to install tree-sitter-agda on Windows 10 (for language-agda). I tried to git clone locally and then npm install. The error log is as follows:

C:\Users\thuzh\tree-sitter-agda\src\parser.c(295,17): error C2001: newline in constant [C:\Users\thuzh\tree-sitter-agda\build\tree_
sitter_agda_binding.vcxproj]
C:\Users\thuzh\tree-sitter-agda\src\parser.c(296,18): error C2001: newline in constant [C:\Users\thuzh\tree-sitter-agda\build\tree_
sitter_agda_binding.vcxproj]
...
C:\Users\thuzh\tree-sitter-agda\src\parser.c(325,18): error C2001: newline in constant [C:\Users\thuzh\tree-sitter-agda\build\tree_
sitter_agda_binding.vcxproj]
C:\Users\thuzh\tree-sitter-agda\src\parser.c(326,18): error C2001: newline in constant [C:\Users\thuzh\tree-sitter-agda\build\tree_
sitter_agda_binding.vcxproj]
...
gyp ERR! build error
gyp ERR! stack Error: `C:\Program Files (x86)\Microsoft Visual Studio\2019\BuildTools\MSBuild\Current\Bin\MSBuild.exe` failed with exit code: 1
gyp ERR! stack     at ChildProcess.onExit (C:\Program Files\nodejs\node_modules\npm\node_modules\node-gyp\lib\build.js:194:23)
gyp ERR! stack     at ChildProcess.emit (events.js:315:20)
gyp ERR! stack     at Process.ChildProcess._handle.onexit (internal/child_process.js:277:12)
gyp ERR! System Windows_NT 10.0.21296
gyp ERR! command "C:\\Program Files\\nodejs\\node.exe" "C:\\Program Files\\nodejs\\node_modules\\npm\\node_modules\\node-gyp\\bin\\node-gyp.js" "rebuild"
gyp ERR! cwd C:\Users\thuzh\tree-sitter-agda
gyp ERR! node -v v14.15.4
gyp ERR! node-gyp -v v5.1.0
gyp ERR! not ok
npm ERR! code ELIFECYCLE
npm ERR! errno 1
npm ERR! [email protected] install: `node-gyp rebuild`
npm ERR! Exit status 1
npm ERR!
npm ERR! Failed at the [email protected] install script.
npm ERR! This is probably not a problem with npm. There is likely additional logging output above.

npm ERR! A complete log of this run can be found in:
npm ERR!     C:\Users\thuzh\AppData\Roaming\npm-cache\_logs\2021-01-29T05_03_56_895Z-debug.log

I looked at the source code and the four lines are pointing to

...
(L295)  [anon_sym_] = "⦃",
(L296)  [anon_sym_2] = "⦄",
...
(L325)  [anon_sym_3] = "⦇",
(L326)  [anon_sym_4] = "⦈",
...

If I delete these four lines, then tree-sitter-agda can be installed successfully and so is language-agda. I guess these four non-ASCII characters are the main cause. Do you have some more elegant way to fix this?

Thanks!

Highlight Set₀ Set₁ ... Setω

From banacorn/language-agda#18 by @zraffer

Perhaps it would be nice to highlight all indexed universe literals Set₀ Set₁ ... Setω (for --omega-in-omega option) the same color as the original unindexed Set literal. Thank you.`

Travis CI

@maxbrunsfeld please help me enable this repo on Travis, thanks! (I don't have sufficient rights to so this)