mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 13:54:55 +03:00
Add optional version tag when build in between releases
Also add REPL :version command to show the current version
This commit is contained in:
parent
4e019d8093
commit
b87fd0beb3
25
Makefile
25
Makefile
@ -2,13 +2,27 @@
|
||||
MAJOR=0
|
||||
MINOR=0
|
||||
PATCH=0
|
||||
IDRIS2_VERSION=${MAJOR}.${MINOR}.${PATCH}
|
||||
|
||||
GIT_SHA1=
|
||||
VER_TAG=
|
||||
ifeq ($(shell git status >/dev/null 2>&1; echo $$?), 0)
|
||||
# inside a git repo
|
||||
ifneq ($(shell git describe --exact-match --tags >/dev/null 2>&1; echo $$?), 0)
|
||||
# not tagged as a released version, so add sha1 of this build in between releases
|
||||
GIT_SHA1 := $(shell git rev-parse --short=9 HEAD)
|
||||
VER_TAG := -${GIT_SHA1}
|
||||
endif
|
||||
endif
|
||||
|
||||
IDRIS2_VERSION=${MAJOR}.${MINOR}.${PATCH}${VER_TAG}
|
||||
|
||||
PREFIX ?= ${HOME}/.idris2
|
||||
IDRIS_VERSION := $(shell idris --version)
|
||||
VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
|
||||
export IDRIS2_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc
|
||||
export IDRIS2_DATA = ${CURDIR}/support
|
||||
|
||||
IDRIS_VERSION := $(shell idris --version)
|
||||
VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
|
||||
|
||||
-include custom.mk
|
||||
|
||||
.PHONY: ttimp idris2 prelude test base clean lib_clean check_version
|
||||
@ -16,14 +30,15 @@ export IDRIS2_DATA = ${CURDIR}/support
|
||||
all: idris2 libs test
|
||||
|
||||
check_version:
|
||||
@echo "Using idris version: $(IDRIS_VERSION)"
|
||||
@echo "Using Idris 1 version: $(IDRIS_VERSION)"
|
||||
@if [ $(shell expr $(IDRIS_VERSION) : $(VALID_IDRIS_VERSION_REGEXP)) -eq 0 ]; then echo "Wrong idris version, expected version matching $(VALID_IDRIS_VERSION_REGEXP)"; exit 1; fi
|
||||
|
||||
idris2: src/YafflePaths.idr check_version
|
||||
@echo "Building Idris 2 version: $(IDRIS2_VERSION)"
|
||||
idris --build idris2.ipkg
|
||||
|
||||
src/YafflePaths.idr:
|
||||
echo 'module YafflePaths; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), "")' > src/YafflePaths.idr
|
||||
echo 'module YafflePaths; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), "${GIT_SHA1}")' > src/YafflePaths.idr
|
||||
echo 'export yprefix : String; yprefix = "${PREFIX}"' >> src/YafflePaths.idr
|
||||
|
||||
prelude:
|
||||
|
@ -80,7 +80,7 @@ atom fname
|
||||
x <- name
|
||||
end <- location
|
||||
pure (PRef (MkFC fname start end) x)
|
||||
|
||||
|
||||
whereBlock : FileName -> Int -> Rule (List PDecl)
|
||||
whereBlock fname col
|
||||
= do keyword "where"
|
||||
@ -105,7 +105,7 @@ continueWith indents req
|
||||
symbol req
|
||||
|
||||
iOperator : Rule Name
|
||||
iOperator
|
||||
iOperator
|
||||
= do n <- operator
|
||||
pure (UN n)
|
||||
<|> do symbol "`"
|
||||
@ -137,13 +137,13 @@ mutual
|
||||
pure (PPrefixOp (MkFC fname start end) op arg)
|
||||
<|> fail "Expected 'case', 'if', 'do', application or operator expression"
|
||||
where
|
||||
applyExpImp : FilePos -> FilePos -> PTerm ->
|
||||
List ArgType ->
|
||||
applyExpImp : FilePos -> FilePos -> PTerm ->
|
||||
List ArgType ->
|
||||
PTerm
|
||||
applyExpImp start end f [] = f
|
||||
applyExpImp start end f (ExpArg exp :: args)
|
||||
= applyExpImp start end (PApp (MkFC fname start end) f exp) args
|
||||
applyExpImp start end f (ImpArg n imp :: args)
|
||||
applyExpImp start end f (ImpArg n imp :: args)
|
||||
= applyExpImp start end (PImplicitApp (MkFC fname start end) f n imp) args
|
||||
applyExpImp start end f (WithArg exp :: args)
|
||||
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
|
||||
@ -187,14 +187,14 @@ mutual
|
||||
opExpr q fname indents
|
||||
= do start <- location
|
||||
l <- appExpr q fname indents
|
||||
(if eqOK q
|
||||
(if eqOK q
|
||||
then do continue indents
|
||||
symbol "="
|
||||
symbol "="
|
||||
r <- opExpr q fname indents
|
||||
end <- location
|
||||
pure (POp (MkFC fname start end) (UN "=") l r)
|
||||
else fail "= not allowed")
|
||||
<|>
|
||||
<|>
|
||||
(do continue indents
|
||||
op <- iOperator
|
||||
middle <- location
|
||||
@ -212,7 +212,7 @@ mutual
|
||||
symbol "**"
|
||||
rest <- dpair fname loc indents <|> expr pdef fname indents
|
||||
end <- location
|
||||
pure (PDPair (MkFC fname start end)
|
||||
pure (PDPair (MkFC fname start end)
|
||||
(PRef (MkFC fname start loc) (UN x))
|
||||
ty
|
||||
rest)
|
||||
@ -345,7 +345,7 @@ mutual
|
||||
<|> do start <- location
|
||||
symbol "["
|
||||
listExpr fname start indents
|
||||
|
||||
|
||||
multiplicity : EmptyRule (Maybe Integer)
|
||||
multiplicity
|
||||
= do c <- intLit
|
||||
@ -360,26 +360,26 @@ mutual
|
||||
getMult Nothing = pure RigW
|
||||
getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"
|
||||
|
||||
pibindAll : FC -> PiInfo -> List (RigCount, Maybe Name, PTerm) ->
|
||||
pibindAll : FC -> PiInfo -> List (RigCount, Maybe Name, PTerm) ->
|
||||
PTerm -> PTerm
|
||||
pibindAll fc p [] scope = scope
|
||||
pibindAll fc p ((rig, n, ty) :: rest) scope
|
||||
= PPi fc rig p n ty (pibindAll fc p rest scope)
|
||||
|
||||
bindList : FileName -> FilePos -> IndentInfo ->
|
||||
bindList : FileName -> FilePos -> IndentInfo ->
|
||||
Rule (List (RigCount, PTerm, PTerm))
|
||||
bindList fname start indents
|
||||
= sepBy1 (symbol ",")
|
||||
(do rigc <- multiplicity
|
||||
pat <- simpleExpr fname indents
|
||||
ty <- option
|
||||
ty <- option
|
||||
(PInfer (MkFC fname start start))
|
||||
(do symbol ":"
|
||||
opExpr pdef fname indents)
|
||||
rig <- getMult rigc
|
||||
pure (rig, pat, ty))
|
||||
|
||||
pibindList : FileName -> FilePos -> IndentInfo ->
|
||||
pibindList : FileName -> FilePos -> IndentInfo ->
|
||||
Rule (List (RigCount, Maybe Name, PTerm))
|
||||
pibindList fname start indents
|
||||
= do rigc <- multiplicity
|
||||
@ -396,7 +396,7 @@ mutual
|
||||
ty <- expr pdef fname indents
|
||||
rig <- getMult rigc
|
||||
pure (rig, Just n, ty))
|
||||
|
||||
|
||||
bindSymbol : Rule PiInfo
|
||||
bindSymbol
|
||||
= do symbol "->"
|
||||
@ -471,7 +471,7 @@ mutual
|
||||
bindAll fc ((rig, pat, ty) :: rest) scope
|
||||
= PLam fc rig Explicit pat ty (bindAll fc rest scope)
|
||||
|
||||
letBinder : FileName -> IndentInfo ->
|
||||
letBinder : FileName -> IndentInfo ->
|
||||
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, List PClause)
|
||||
letBinder fname indents
|
||||
= do start <- location
|
||||
@ -490,7 +490,7 @@ mutual
|
||||
buildLets fname [] sc = sc
|
||||
buildLets fname ((start, end, rig, pat, val, alts) :: rest) sc
|
||||
= let fc = MkFC fname start end in
|
||||
PLet fc rig pat (PImplicit fc) val
|
||||
PLet fc rig pat (PImplicit fc) val
|
||||
(buildLets fname rest sc) alts
|
||||
|
||||
buildDoLets : FileName ->
|
||||
@ -501,7 +501,7 @@ mutual
|
||||
= let fc = MkFC fname start end in
|
||||
if lowerFirst n
|
||||
then DoLet fc (UN n) rig val :: buildDoLets fname rest
|
||||
else DoLetPat fc (PRef fc' (UN n)) val []
|
||||
else DoLetPat fc (PRef fc' (UN n)) val []
|
||||
:: buildDoLets fname rest
|
||||
buildDoLets fname ((start, end, rig, pat, val, alts) :: rest)
|
||||
= let fc = MkFC fname start end in
|
||||
@ -511,12 +511,12 @@ mutual
|
||||
let_ fname indents
|
||||
= do start <- location
|
||||
keyword "let"
|
||||
res <- nonEmptyBlock (letBinder fname)
|
||||
res <- nonEmptyBlock (letBinder fname)
|
||||
commitKeyword indents "in"
|
||||
scope <- typeExpr pdef fname indents
|
||||
end <- location
|
||||
pure (buildLets fname res scope)
|
||||
|
||||
|
||||
<|> do start <- location
|
||||
keyword "let"
|
||||
commit
|
||||
@ -541,13 +541,13 @@ mutual
|
||||
= do start <- location
|
||||
lhs <- opExpr plhs fname indents
|
||||
caseRHS fname start indents lhs
|
||||
|
||||
|
||||
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause
|
||||
caseRHS fname start indents lhs
|
||||
= do symbol "=>"
|
||||
mustContinue indents Nothing
|
||||
rhs <- expr pdef fname indents
|
||||
atEnd indents
|
||||
atEnd indents
|
||||
end <- location
|
||||
pure (MkPatClause (MkFC fname start end) lhs rhs [])
|
||||
<|> do keyword "impossible"
|
||||
@ -597,7 +597,7 @@ mutual
|
||||
tm <- expr pdef fname indents
|
||||
end <- location
|
||||
pure (PRewrite (MkFC fname start end) rule tm)
|
||||
|
||||
|
||||
doBlock : FileName -> IndentInfo -> Rule PTerm
|
||||
doBlock fname indents
|
||||
= do start <- location
|
||||
@ -660,7 +660,7 @@ mutual
|
||||
patAlt fname indents
|
||||
= do symbol "|"
|
||||
caseAlt fname indents
|
||||
|
||||
|
||||
lazy : FileName -> IndentInfo -> Rule PTerm
|
||||
lazy fname indents
|
||||
= do start <- location
|
||||
@ -707,8 +707,8 @@ mutual
|
||||
where
|
||||
mkPi : FilePos -> FilePos -> PTerm -> List (PiInfo, PTerm) -> PTerm
|
||||
mkPi start end arg [] = arg
|
||||
mkPi start end arg ((exp, a) :: as)
|
||||
= PPi (MkFC fname start end) RigW exp Nothing arg
|
||||
mkPi start end arg ((exp, a) :: as)
|
||||
= PPi (MkFC fname start end) RigW exp Nothing arg
|
||||
(mkPi start end a as)
|
||||
|
||||
export
|
||||
@ -780,7 +780,7 @@ mutual
|
||||
applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args
|
||||
|
||||
parseWithArg : Rule (FC, PTerm)
|
||||
parseWithArg
|
||||
parseWithArg
|
||||
= do symbol "|"
|
||||
start <- location
|
||||
tm <- expr plhs fname indents
|
||||
@ -789,7 +789,7 @@ mutual
|
||||
|
||||
mkTyConType : FC -> List Name -> PTerm
|
||||
mkTyConType fc [] = PType fc
|
||||
mkTyConType fc (x :: xs)
|
||||
mkTyConType fc (x :: xs)
|
||||
= PPi fc Rig1 Explicit Nothing (PType fc) (mkTyConType fc xs)
|
||||
|
||||
mkDataConType : FC -> PTerm -> List ArgType -> PTerm
|
||||
@ -798,9 +798,9 @@ mkDataConType fc ret (ExpArg x :: xs)
|
||||
= PPi fc Rig1 Explicit Nothing x (mkDataConType fc ret xs)
|
||||
mkDataConType fc ret (ImpArg n (PRef fc' x) :: xs)
|
||||
= if n == Just x
|
||||
then PPi fc Rig1 Implicit n (PType fc')
|
||||
then PPi fc Rig1 Implicit n (PType fc')
|
||||
(mkDataConType fc ret xs)
|
||||
else PPi fc Rig1 Implicit n (PRef fc' x)
|
||||
else PPi fc Rig1 Implicit n (PRef fc' x)
|
||||
(mkDataConType fc ret xs)
|
||||
mkDataConType fc ret (ImpArg n x :: xs)
|
||||
= PPi fc Rig1 Implicit n x (mkDataConType fc ret xs)
|
||||
@ -816,7 +816,7 @@ simpleCon fname ret indents
|
||||
atEnd indents
|
||||
end <- location
|
||||
let cfc = MkFC fname start end
|
||||
pure (MkPTy cfc cname (mkDataConType cfc ret params))
|
||||
pure (MkPTy cfc cname (mkDataConType cfc ret params))
|
||||
|
||||
simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
|
||||
simpleData fname start n indents
|
||||
@ -826,7 +826,7 @@ simpleData fname start n indents
|
||||
symbol "="
|
||||
let conRetTy = papply tyfc (PRef tyfc n)
|
||||
(map (PRef tyfc) params)
|
||||
cons <- sepBy1 (symbol "|")
|
||||
cons <- sepBy1 (symbol "|")
|
||||
(simpleCon fname conRetTy indents)
|
||||
end <- location
|
||||
pure (MkPData (MkFC fname start end) n
|
||||
@ -840,7 +840,7 @@ dataOpt
|
||||
ns <- some name
|
||||
pure (SearchBy ns)
|
||||
|
||||
dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm ->
|
||||
dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm ->
|
||||
EmptyRule PDataDecl
|
||||
dataBody fname mincol start n indents ty
|
||||
= do atEndIndent indents
|
||||
@ -868,7 +868,7 @@ dataDeclBody fname indents
|
||||
col <- column
|
||||
keyword "data"
|
||||
n <- name
|
||||
simpleData fname start n indents
|
||||
simpleData fname start n indents
|
||||
<|> gadtData fname col start n indents
|
||||
|
||||
dataDecl : FileName -> IndentInfo -> Rule PDecl
|
||||
@ -887,8 +887,8 @@ stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
|
||||
drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs
|
||||
|
||||
onoff : Rule Bool
|
||||
onoff
|
||||
= do exactIdent "on"
|
||||
onoff
|
||||
= do exactIdent "on"
|
||||
pure True
|
||||
<|> do exactIdent "off"
|
||||
pure False
|
||||
@ -965,7 +965,7 @@ fix
|
||||
<|> do keyword "prefix"; pure Prefix
|
||||
|
||||
namespaceHead : Rule (List String)
|
||||
namespaceHead
|
||||
namespaceHead
|
||||
= do keyword "namespace"
|
||||
commit
|
||||
ns <- namespace_
|
||||
@ -1038,7 +1038,7 @@ visOpt
|
||||
opt <- fnDirectOpt
|
||||
pure (Right opt)
|
||||
|
||||
getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
|
||||
getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
|
||||
EmptyRule Visibility
|
||||
getVisibility Nothing [] = pure Private
|
||||
getVisibility (Just vis) [] = pure vis
|
||||
@ -1112,7 +1112,7 @@ ifaceDecl fname indents
|
||||
pure (Just n))
|
||||
body <- assert_total (blockAfter col (topDecl fname))
|
||||
end <- location
|
||||
pure (PInterface (MkFC fname start end)
|
||||
pure (PInterface (MkFC fname start end)
|
||||
vis cons n params det dc (collectDefs (concat body)))
|
||||
|
||||
implDecl : FileName -> IndentInfo -> Rule PDecl
|
||||
@ -1134,7 +1134,7 @@ implDecl fname indents
|
||||
atEnd indents
|
||||
end <- location
|
||||
pure (PImplementation (MkFC fname start end)
|
||||
vis Single impls cons n params iname
|
||||
vis Single impls cons n params iname
|
||||
(map (collectDefs . concat) body))
|
||||
|
||||
fieldDecl : FileName -> IndentInfo -> Rule (List PField)
|
||||
@ -1176,7 +1176,7 @@ recordDecl fname indents
|
||||
keyword "where"
|
||||
dcflds <- blockWithOptHeaderAfter col ctor (fieldDecl fname)
|
||||
end <- location
|
||||
pure (PRecord (MkFC fname start end)
|
||||
pure (PRecord (MkFC fname start end)
|
||||
vis n params (fst dcflds) (concat (snd dcflds)))
|
||||
where
|
||||
ctor : IndentInfo -> Rule Name
|
||||
@ -1196,7 +1196,7 @@ claim fname indents
|
||||
cl <- tyDecl fname indents
|
||||
end <- location
|
||||
pure (PClaim (MkFC fname start end) rig vis opts cl)
|
||||
|
||||
|
||||
definition : FileName -> IndentInfo -> Rule PDecl
|
||||
definition fname indents
|
||||
= do start <- location
|
||||
@ -1217,7 +1217,7 @@ fixDecl fname indents
|
||||
directiveDecl : FileName -> IndentInfo -> Rule PDecl
|
||||
directiveDecl fname indents
|
||||
= do start <- location
|
||||
symbol "%"
|
||||
symbol "%"
|
||||
(do d <- directive fname indents
|
||||
end <- location
|
||||
pure (PDirective (MkFC fname start end) d))
|
||||
@ -1283,8 +1283,8 @@ collectDefs (PDef annot cs :: ds)
|
||||
(ys, zs) => (y ++ ys, zs)
|
||||
|
||||
isClause : PDecl -> Maybe (List PClause)
|
||||
isClause (PDef annot cs)
|
||||
= Just cs
|
||||
isClause (PDef annot cs)
|
||||
= Just cs
|
||||
isClause _ = Nothing
|
||||
collectDefs (PNamespace annot ns nds :: ds)
|
||||
= PNamespace annot ns (collectDefs nds) :: collectDefs ds
|
||||
@ -1353,7 +1353,7 @@ setVarOption
|
||||
mode <- parseMode
|
||||
pure (EvalMode mode)
|
||||
<|> do exactIdent "editor"
|
||||
e <- unqualifiedName
|
||||
e <- unqualifiedName
|
||||
pure (Editor e)
|
||||
<|> do exactIdent "cg"
|
||||
c <- unqualifiedName
|
||||
@ -1462,6 +1462,8 @@ nonEmptyCommand
|
||||
pure (SetLog (fromInteger i))
|
||||
<|> do symbol ":"; replCmd ["m", "metavars"]
|
||||
pure Metavars
|
||||
<|> do symbol ":"; replCmd ["version"]
|
||||
pure ShowVersion
|
||||
<|> do symbol ":"; cmd <- editCmd
|
||||
pure (Editing cmd)
|
||||
<|> do tm <- expr pdef "(interactive)" init
|
||||
|
@ -568,7 +568,8 @@ process NOP
|
||||
process ShowVersion
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ => iputStrLn $ showVersion version
|
||||
REPL _ => do iputStrLn $ showVersion version
|
||||
pure True
|
||||
IDEMode i _ f => do
|
||||
let MkVersion (maj, min, patch) t = version
|
||||
send f (SExpList [SymbolAtom "return",
|
||||
@ -576,7 +577,7 @@ process ShowVersion
|
||||
SExpList [SExpList (map (IntegerAtom . cast) [maj, min, patch]),
|
||||
SExpList [ StringAtom $ fromMaybe "" t ]]],
|
||||
toSExp i])
|
||||
pure False
|
||||
pure False
|
||||
|
||||
processCatch : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
|
2
tests/ideMode/ideMode002/.gitignore
vendored
Normal file
2
tests/ideMode/ideMode002/.gitignore
vendored
Normal file
@ -0,0 +1,2 @@
|
||||
/expected
|
||||
|
@ -1,3 +1,3 @@
|
||||
000018(:protocol-version 2 0)
|
||||
000021(:return (:ok ((0 0 0) (""))) 1)
|
||||
__EXPECTED_LINE__
|
||||
Alas the file is done, aborting
|
15
tests/ideMode/ideMode002/gen_expected.sh
Executable file
15
tests/ideMode/ideMode002/gen_expected.sh
Executable file
@ -0,0 +1,15 @@
|
||||
#!/usr/bin/env sh
|
||||
|
||||
INPUT=`cat`
|
||||
|
||||
VERSION=`echo $INPUT | cut -d- -f1`
|
||||
TAG=`echo $INPUT | cut -s -d- -f2`
|
||||
|
||||
MAJOR=`echo $VERSION | cut -d. -f1`
|
||||
MINOR=`echo $VERSION | cut -d. -f2`
|
||||
PATCH=`echo $VERSION | cut -d. -f3`
|
||||
|
||||
EXPECTED_LINE="(:return (:ok ((${MAJOR} ${MINOR} ${PATCH}) (\"${TAG}\"))) 1)"
|
||||
EXPECTED_LENGTH=$(expr ${#EXPECTED_LINE} + 1) # +LF
|
||||
|
||||
sed -e "s/__EXPECTED_LINE__/$(printf '%06x' ${EXPECTED_LENGTH})${EXPECTED_LINE}/g" expected.in > expected
|
@ -1,3 +1,4 @@
|
||||
$1 --version | awk '{print $4}' | ./gen_expected.sh
|
||||
$1 --ide-mode < input
|
||||
|
||||
rm -rf build
|
||||
|
Loading…
Reference in New Issue
Block a user