`Vatras` module
Closed this issue · 3 comments
pmbittner commented
Currently, we do not have a common module for our files. These all just live directly in src
and not in a grouping module. This limits reusability in other libraries and also leads to anomalies such as Data.IndexedSet
reading the same as imports from the standard library (e.g., Data.Nat
).
We should move all files in src
to src/Vatras
and rename the module definitions accordingly.
ibbem commented
You can use
cd src
rg '^ *module ' | awk -v FS=: '{ if ($1 != previous) { previous=$1; print $2 } }' | sed 's/module *\([^ ]*\).*/\1/' | awk '{ escaped=$0; gsub("\\.", "\\.", escaped); print "sed -i -e '\''s/ \\(" escaped "\\)/ Vatras.\\1/g'\'' \"$1\"" }' > commands
mkdir Vatras
find . -mindepth 1 -maxdepth 1 -not \( -name "Vatras" -o -name "commands" \) -exec mv -t Vatras {} +
find . -name '*agda*' -exec bash commands {} \;
to move everything into a Vatras
module. The only module that needs manual adjusting is Main
.
pmbittner commented
Thanks! Let's do this after the submission to not accidentally break any links in the README on the last meters.
pmbittner commented
Please also remember to update the README.