Extract regexp for .ipkg sourcedir option to constant and update the regexp to include also double quotes.

[keram]

Why:

In Idris2 the sourcedir option has double quotes.

Relates to: https://github.com/idris-hackers/idris-mode/issues/624

It seems to resolve the second reported issue of flycheck reporting issue "Module name X does not match file Y"

[jfdm]

@keram thanks for this! I see that the tests are failing, and acknowledge that this is not an issue with this PR. I will look to address the failing tests the now, and will merge your PR. Thanks!

[dunhamsteve]

With idris2, this seems to be causing an error:

Error: Source file "Main.idr" is not in the source directory "/Users/dunham/prj/idris/scratch/src"

for me and a couple of other users on discord. Reverting to the previous commit, aa580b6, resolves the regression.

This is happening for a pack-generated project, loading Main.idr in the source directory and attempting to invoke C-c C-l.

[jfdm]

@dunhamsteve thanks for highlighting this issue.

I have reverted the regexp in a separate PR (i like the extraction).

The reason this was not being discovered in our tests is that our tests to do cover loading projects with source dirs. The test suite is lightweight afterall.

I tried reproducing the error as a test in ert, alas I could not do so. In the interest of a working version on melpa, I reverted the new regexp.

[keram]

Hi @dunhamstev @jfdm Sorry for the regression! I was aware of issues though didn't expect them to affect others. ;/ In reality there is no isssue with the regexp or the idris-mode but in the Idris2 itself. In short the Idris2 tries to load the file relatively to the "working directory" instead of relatively to "source directory". This is clearly incorrect as even the error message Source file "Main.idr" is not in the source directory "/Users/dunham/prj/idris/scratch/src" suggest that it should look up the Main.idr relatively to the source dir (src). I reported the issue here https://github.com/idris-lang/Idris2/issues/3310 and as exercise started looking into fixing that but with no luck and much time recently ;/.

Said that I started also working on improving handling of "working dir", "source dir", "ipkg files in the idris-mode.

[dunhamsteve]

I think that error message was the version you get when there actually is an additional Main.idr in the parent directory. I had run both scenarios.

Two distinct regular expressions were merged in the PR. One allowed _ in the path and spaces in front of sourcedir, and the other allows / in the path. I'm guessing much more than \w is accepted, but other characters would be rare. I think idris-mode worked with Idris2 because neither regex ever matched anything. Maybe it was used by idris1?

It looks like, when loading a file, Idris will set the current working directory to the directory containing the appropriate .ipkg file. And I think it then expects the filename to be relative to the ipkg. (Although it also seems to accept absolute path names.) That's line 1040 of src/Idris/Package.idr and the commit comment says that it was put there by Edwin to make the vim-mode work. (Note that having two .ipkg in one directory is a problem for everybody, and I think we're trying to avoid it for now.)

If we didn't want to change Idris, we could try loading an absolute path. It seems to work at the REPL.

Otherwise, it might work to prepare a path relative to the appropriate .ipkg file, and change the working directory to the ipkg directory before loading an ipkg relative path.

If we do change Idris, we'll have to figure out what breaks when the current working directory is not changed to the package root and fix it. (Double checking LSP and non-lsp editor modes - I think vim is the only one.)

[keram]

I think that error message was the version you get when there actually is an additional Main.idr in the parent directory. I had run both scenarios.

Will check but I'm not aware of this.

Two distinct regular expressions were merged in the PR. One allowed _ in the path and spaces in front of sourcedir, and the other allows / in the path.

Yes, previously we had 2 different RegExp-s used in two different contexts trying to do the same job.

I'm guessing much more than \w is accepted, but other characters would be rare.

Good point that once we removed the duplication using the one with \sw+ instead of [a-zA-Z/0-9]+ is less restrictive and we may want to switch to it.

I think idris-mode worked with Idris2 because neither regex ever matched anything. Maybe it was used by idris1?

Exactly! idris-mode & ipkg file is kind of working with the "incorrect Idris2 implementation" because of the regexp was not recognising the new syntax using double quotes. Idris1 ipkg file:

sourcedir = src

Idris2 ipkg file

sourcedir = "src"

It looks like, when loading a file, Idris will set the current working directory to the directory containing the appropriate .ipkg file.

This is good and I think also that in Idris2 is better distinction between "working directory" and "source directory". It seems that in Idris1 wasn't clear distinction and for that reasons the idris-mode tries to always switch the working directory releatively to the currently loaded file.

And I think it then expects the filename to be relative to the ipkg. (Although it also seems to accept absolute path names.) That's line 1040 of src/Idris/Package.idr and the commit comment says that it was put there by Edwin to make the vim-mode work. (Note that having two .ipkg in one directory is a problem for everybody, and I think we're trying to avoid it for now.)

Will update later which part I identified that may need to be improved. (have that on different computer)

If we didn't want to change Idris, we could try loading an absolute path. It seems to work at the REPL.

Funnily that is a workaround in my idris-mode devel branch I used https://github.com/keram/idris-mode/commit/afa99a32de6427efc14188385a9cf2da12849807#diff-57c9b17a4d33ee59f640d96a562f576b22d600b5adb02038a989e8eb1d2e76c5R171 (Though using absolute path is just workaround and not long term fix as it itself has some disadvantages.) There in the diff you can see also where this regression is comming from. Old code: https://github.com/keram/idris-mode/commit/afa99a32de6427efc14188385a9cf2da12849807#diff-57c9b17a4d33ee59f640d96a562f576b22d600b5adb02038a989e8eb1d2e76c5L172-L176

(defun idris-filename-to-load () ...
(let* ((fn (buffer-file-name))
         (ipkg-srcdir (idris-ipkg-find-src-dir))
         (srcdir (or ipkg-srcdir (file-name-directory fn))))
    (when (and  ;; check that srcdir is prefix of filename - then load relative
           (> (length fn) (length srcdir))
           (string= (substring fn 0 (length srcdir)) srcdir))
      (setq fn (file-relative-name fn srcdir)))
    (cons srcdir fn)))

Once the idris-mode started detecting correctly the ipkg sourcedir value it is stripped from the path to load which was/is expected behaviour for the Idris1.

Otherwise, it might work to prepare a path relative to the appropriate .ipkg file, and change the working directory to the ipkg directory before loading an ipkg relative path.

If we do change Idris, we'll have to figure out what breaks when the current working directory is not changed to the package root and fix it. (Double checking LSP and non-lsp editor modes - I think vim is the only one.)

My proposal and direction I'm working on is:

1. Revert of revert of the regexp and implement instead a workaround in the idris-filename-to-load for the IDE protocol version greater than 1.

   (Having the correct regexp enables another functionalities in the ide-mode and Emacs )

2. Implement fix in Idris2 which would be released as "breaking change" and such would be released as new version of the IDE mode protocol.

3. In idris-mode & idris-filename-to-load detect the version of the IDE protocol with the fix and based on that use the correct behaviour.