IdrisNet2
IdrisNet2 copied to clipboard
Fails to compile on idris 1.0
I was able to fix a small compiling error on my own:
--- a/src/IdrisNet/PacketLang.idr
+++ b/src/IdrisNet/PacketLang.idr
@@ -163,7 +163,7 @@ syntax lstring [n] = (CHUNK (LString n))
syntax cstring = (CHUNK (CString))
syntax listn [n] [t] = (LISTN n t)
syntax list [t] = (LIST t)
-syntax p_if [b1] then [b2] else [b3] = (IF b1 b2 b3)
+syntax p_if [b1] "then" [b2] "else" [b3] = (IF b1 b2 b3)
syntax p_either [t1] [t2] = (t1 // t2)
syntax bool = (CHUNK (CBool))
syntax prop [p] = (CHUNK (Prop p))
Also there have been some warnings because of the use of public
instead of publix export
.
But now I do get the following:
make
idris --build network.ipkg
Entering directory `./src'
make[1]: Entering directory '/home/nmelzer/projects/idris/IdrisNet2/src'
make[1]: Nothing to be done for 'all'.
make[1]: Leaving directory '/home/nmelzer/projects/idris/IdrisNet2/src'
Type checking ./IdrisNet/Packet.idr
./IdrisNet/Packet.idr:28:19:When checking type of IdrisNet.Packet.ActivePacketRes:
No such variable BufPtr
./IdrisNet/Packet.idr:31:12:When checking type of IdrisNet.Packet.dumpPacket:
No such variable BufPtr
Makefile:2: recipe for target 'all' failed
make: *** [all] Error 1
Which I'm not able to solve on my own.
Perhaps there will be even more stuff braking compilation once this file got fixed...
problem is still actual for idris 1.3.0