Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fails to compile on idris 1.0 #13

Open
NobbZ opened this issue Jun 3, 2017 · 1 comment
Open

Fails to compile on idris 1.0 #13

NobbZ opened this issue Jun 3, 2017 · 1 comment

Comments

@NobbZ
Copy link

NobbZ commented Jun 3, 2017

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

@andreykl
Copy link

problem is still actual for idris 1.3.0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants