@mflatt I’m trying to install racket3m from the source snapshot . When running make install I get an error in line <https://github.com/racket/racket/blob/ced16f686875466f3db33a4ad85789c28d9f1d3f/racket/src/racket/Makefile.in#L450|line 450 of the makefile> (added in commit https://github.com/racket/racket/commit/2de28c8cf3effab7c3a3cfef89362122861de659\|2de28c8 ) with following output cd ..; libtool --mode=install install -s rktio/librktio.la "/home/bert/builds/racket-snap/pkg/racket/usr/lib/librktio.la" libtool: install: install rktio/.libs/librktio.lai /home/bert/builds/racket-snap/pkg/racket/usr/lib/librktio.la install: cannot stat 'rktio/.libs/librktio.lai': No such file or directory I don’t know if it’s relevant but if I look into http://librktio.la\|librktio.la, all fields are empty except for old_library, installed(=no) and shouldnotlink(=no)

If there is any extra info I could provide please let me know

I’ve pushed a repair for make install in --enable-shared mode. As a workaround for now, you could just delete the offending makefile line.

thanks!

My new flânerie, Logic and Computation Intertwined, is up. https://cs.uwaterloo.ca/~plragde/flaneries/LACI/

I spoke on this at RacketCon 2017. It has the reader use Racket to construct a very small dependently-typed proof assistant in order to study propositional and predicate logic. There are also introductions to Agda and Coq. The Racket code isn’t at all fancy, but that’s the point.

https://cs.uwaterloo.ca/~plragde/flaneries/LACI/halting.html is 403 Forbidden

Thanks! Fixed.

can someone explain how to read this unbound id error? Especially: what does “other binding” mean?

g3083: unbound identifier in: g3083 context...: #(-13660 module core) #(-13657 module) [common scopes] other binding...: #(g3083.1 #<module-path-index=(submod 'data[8502] #%type-decl)> 0) #(-14375 module init-envs) #(-14372 module) #(12622 macro) [common scopes] common scopes...: #(12620 module data) #(16802 module) #(16810 module #%type-decl)

For context, I’m inside typed racket. Early on, it makes a submodule named #%type-decl. I’m trying to put more code into that submodule. I want to introduce a reference to a g3083 that’s defined earlier in the submodule.

It says that an identifier g3083 almost refers to a binding for g3083 within a #%type-decl submodule. The binding has additional scopes, though, that make it not bind the reference: a macro-induction scope and the scope of a module name init-envs.

thanks

I’m going to try a different approach now, without injecting code

But I’m confused about how to get the init-envs scope. That g3083 is coming from init-envs in both cases (the second time from a cache). How would I try to add that scope?

You’re stashing an identifier in a cache? Are you using syntax-local-introduce on the cached identifier?

it’s a gensym in the cache .. but ok, there’s nearby syntax and no syntax-local-introduce in the file — so that sounds good, I can try adding introducers

I’ve seen the VOD on youtube, Proust or something like that, right?

Good work :slightly_smiling_face: !