IdrisNet2 icon indicating copy to clipboard operation
IdrisNet2 copied to clipboard

Fails to compile on idris 1.0

Open NobbZ opened this issue 7 years ago • 1 comments

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...

NobbZ avatar Jun 03 '17 09:06 NobbZ

problem is still actual for idris 1.3.0

andreykl avatar Dec 21 '18 20:12 andreykl