Closed mariari closed 1 year ago
Thanks for the pr @mariari.
There is some context to give about juvix-input.el
. This file was copied from the Agda repo.
We did a basic search and replace to subsitute agda
by juvix
in the function names and possibly other minor changes that I don't remember. Our intention is to not manually maintain our copy of juvix-input.el
. Instead, we will periodically copy the file again from the Agda repo. Of course, it would be nice to have some sort of script that adapts to file automatically, but we haven't come to that yet. As a consequence, the changes you did in juvix-input.el
will be overwritten at some point. What I would suggest (if you want to do so), is that you commit future changes in the juvix-input.el
file directly to agda-input.el
of the Agda repo.
Thanks for the pr @mariari.
There is some context to give about
juvix-input.el
. This file was copied from the Agda repo. We did a basic search and replace to subsituteagda
byjuvix
in the function names and possibly other minor changes that I don't remember. Our intention is to not manually maintain our copy ofjuvix-input.el
. Instead, we will periodically copy the file again from the Agda repo. Of course, it would be nice to have some sort of script that adapts to file automatically, but we haven't come to that yet. As a consequence, the changes you did injuvix-input.el
will be overwritten at some point. What I would suggest (if you want to do so), is that you commit future changes in thejuvix-input.el
file directly toagda-input.el
of the Agda repo.
I believe there is a better way to include this kind of application in the Juvix emacs mode.
Either:
agda-input-mode
as your input modeagda-input-mode
one implies no fork. and three may be the right choice as agda
's input mode is universal and works in other modes fine (I know someone who uses it as their default unicodefier for emacs operations), and Juvix requires no unicode to write nor use.
As for two, there are good ways for working with it. You can do something similar to
% git pull --allow-unrelated-histories --no-ff -s ours --no-commit ../vendoree v1.0.0
% git read-tree -u --prefix=vendored/lib/ FETCH_HEAD
% git log
* 7229065 (HEAD -> master) Vendor lib 1.0.0
|\
| * 4b068c5 version 1.0.0
* 8963346 initial commit
then you can merge like
git pull --no-ff -s subtree ../vendoree v1.1.0
% git log
* 4c45700 (HEAD -> master) Merge tag 'v1.1.0' of ../vendoree into master
|\
| * b5de266 Version 1.1.0
* | 7229065 Vendor lib 1.0.0
|\|
| * 4b068c5 version 1.0.0
* 8963346 initial commit
then the customization are just merged like they are here
This PR properly formats the lisp and hopefully makes the code a bit clearer.
Please try it out before merging