cpet/freebsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

math/hs-Agda: Unbreak and enable compiling emacs mode files.

Browse Source
This commit is contained in:
Gleb Popov 2022-08-15 16:06:51 +03:00
parent 1418764bb1
commit a04537df06
3 changed files with 35 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
math/hs-Agda/Makefile
View File

@ -1,6 +1,6 @@
PORTNAME= Agda
PORTVERSION= 2.6.2.2
PORTREVISION= 1
PORTREVISION= 2
CATEGORIES= math haskell
MAINTAINER= haskell@FreeBSD.org
@ -82,18 +82,15 @@ USE_CABAL= OneTuple-0.3.1_2 \
witherable-0.4.2_2 \
zlib-0.6.3.0
EXECUTABLES= agda-mode agda
CABAL_WRAPPER_SCRIPTS= ${EXECUTABLES}
CABAL_EXECUTABLES= agda-mode agda
CABAL_WRAPPER_SCRIPTS= ${CABAL_EXECUTABLES}
agda_DATADIR_VARS= Agda
agda-mode_DATADIR_VARS= Agda
post-build:
# Do not compile Emacs mode files until https://github.com/agda/agda/issues/4610 is fixed
# ${SETENV} Agda_datadir=${WRKSRC}/src/data $$(find ${WRKSRC}/dist-newstyle -name agda-mode -type f -perm +111) compile
post-install:
${SETENV} Agda_datadir=${WRKSRC}/src/data ${STAGEDIR}${PREFIX}/libexec/cabal/agda-mode compile
find ${WRKSRC}/src/data/lib/prim/Agda -name '*.agda' -exec ${SETENV} Agda_datadir=${WRKSRC}/src/data ${STAGEDIR}${PREFIX}/libexec/cabal/agda {} \;
${MKDIR} ${STAGEDIR}${DATADIR}/lib/prim/Agda
find ${WRKSRC}/src/data/lib/prim/Agda -name '*.agda' -exec ${SETENV} ${PORTNAME}_datadir=${WRKSRC}/src/data ${STAGEDIR}${PREFIX}/libexec/cabal/agda {} \;
cd ${WRKSRC}/src/data && ${COPYTREE_SHARE} lib ${STAGEDIR}${DATADIR}
cd ${WRKSRC}/src/data && ${COPYTREE_SHARE} emacs-mode ${STAGEDIR}${DATADIR}

22
math/hs-Agda/files/patch-src_data_emacs-mode_agda2-mode.el Normal file
View File

@ -0,0 +1,22 @@
--- src/data/emacs-mode/agda2-mode.el.orig 2001-09-09 01:46:40 UTC
+++ src/data/emacs-mode/agda2-mode.el
@@ -1306,7 +1306,8 @@ top-level scope."
(agda2-maybe-normalised
agda2-elaborate-give
- "Elaborate check the given expression against the hole's type and fill in hole with the elaborated term"
+ "Elaborate check the given expression against the hole's type and fill
+in hole with the elaborated term"
"Cmd_elaborate_give"
"expression to elaborate and give")
@@ -1324,7 +1325,8 @@ top-level scope."
(agda2-maybe-normalised
agda2-goal-and-context-and-checked
- "Shows the context, the goal and check the given expression's against the hole's type"
+ "Shows the context, the goal and check the given expression's against
+the hole's type"
"Cmd_goal_type_context_check"
"expression to type")

8
math/hs-Agda/pkg-plist
View File

@ -1,12 +1,20 @@
%%DATADIR%%/emacs-mode/agda-input.el
%%DATADIR%%/emacs-mode/agda-input.elc
%%DATADIR%%/emacs-mode/agda2-abbrevs.el
%%DATADIR%%/emacs-mode/agda2-abbrevs.elc
%%DATADIR%%/emacs-mode/agda2-highlight.el
%%DATADIR%%/emacs-mode/agda2-highlight.elc
%%DATADIR%%/emacs-mode/agda2-mode-pkg.el
%%DATADIR%%/emacs-mode/agda2-mode.el
%%DATADIR%%/emacs-mode/agda2-mode.elc
%%DATADIR%%/emacs-mode/agda2-queue.el
%%DATADIR%%/emacs-mode/agda2-queue.elc
%%DATADIR%%/emacs-mode/agda2.el
%%DATADIR%%/emacs-mode/agda2.elc
%%DATADIR%%/emacs-mode/annotation.el
%%DATADIR%%/emacs-mode/annotation.elc
%%DATADIR%%/emacs-mode/eri.el
%%DATADIR%%/emacs-mode/eri.elc
%%DATADIR%%/lib/prim/Agda/Builtin/Bool.agda
%%DATADIR%%/lib/prim/Agda/Builtin/Bool.agdai
%%DATADIR%%/lib/prim/Agda/Builtin/Char.agda