Re: [racket-users] ARM32 binaries for CS, or building on ARM 32
I'm on an old RPi B (maybe a B+). It's pretty ancient, so I might be pushing my luck. Here's my CPU info: pi@raspberrypi:~ $ cat /proc/cpuinfo processor: 0 model name: ARMv6-compatible processor rev 7 (v6l) BogoMIPS: 697.95 Features: half thumb fastmult vfp edsp java tls CPU implementer: 0x41 CPU architecture: 7 CPU variant: 0x0 CPU part: 0xb76 CPU revision: 7 Hardware: BCM2835 Revision: 000e Serial: e9b1ce2d Model: Raspberry Pi Model B Rev 2 Running GDB gives the illegal instruction as instruction: 0xf57ff05a which looks to be a "Data Memory Barrier" instruction? Sounds like a plausible culprit. Thanks! On Tuesday, August 11, 2020 at 2:14:28 PM UTC-7, Matthew Flatt wrote: > > Which model Pi are you using? I'm able to build on a Pi 3, so I wonder > if it's a difference in processors, where the Arm32 backend is using > something that it shouldn't. > > Whether or not that guess is right, can you try running `gdb` in the > "ChezScheme" directory like this? > >env SCHEMEHEAPDIRS=tarm32le/boot/tarm32le/ \ > gdb tarm32le/bin/tarm32le/scheme > > Disassembling around the failed instruction address (with `disassemble` > in gdb) should clarify what instruction is misused. > > Thanks, > Matthew > > At Tue, 11 Aug 2020 10:58:03 -0700 (PDT), Joey Eremondi wrote: > > I'm wondering, does anybody have any prebuilt 32-but ARM binaries for > > Racket on Chez? I'm trying to run a little web-server on a raspberry pi, > > and I'd prefer to use the Chez version, but I can't seem to get it to > build. > > > > Alternately, if anybody knows why it won't build and can help, that > would > > help. With eiether --enable-csracket or --enable-csonly, it gets stuck > > compiling the forked version of ChezScheme. Surprisingly, it doesn't > seem > > to be an out of memory error. Is the illegal instruction error because > it's > > ARMv6 and not AArch32? > > > > ... > > gcc -Wpointer-arith -Wextra -Werror -Wno-implicit-fallthrough -O2 -g > -O2 - > > Wall -DELF_FIND_BOOT_SECTION -pthread -rdynamic -o > ../bin/tarm32le/scheme > > ../boot/tarm32le/main.o ../boot/tarm32le/libkernel.a -lm -ldl -lpthread > -lrt > > -luuid ../zlib/libz.a ../lz4/lib/liblz4.a -pthread > > (cd s && make bootstrap) > > make allx > > rm -f *.tarm32le xpatch patch *.patch *.so *.covin *.asm script.all > header.tmp > > *.html > > rm -rf nanopass > > cp -p -f ../boot/tarm32le/petite.boot ../boot/tarm32le/sbb > > cp -p -f ../boot/tarm32le/scheme.boot ../boot/tarm32le/scb > > make all > > echo '(reset-handler abort)'\ > > '(base-exception-handler (lambda (c) (fresh-line) > > (display-condition c) (newline) (reset)))'\ > > '(keyboard-interrupt-handler (lambda () (display > > "interrupted---aborting\n") (reset)))'\ > > '(optimize-level 3)'\ > > '(debug-level 0)'\ > > '(commonization-level (commonization-level))'\ > > '(compile-compressed #t)'\ > > '(compress-format (compress-format))'\ > > '(compress-level (compress-level))'\ > > '(generate-inspector-information #f)'\ > > '(subset-mode (quote system))'\ > > '(compile-file "cmacros.ss" "cmacros.so")'\ > > | ../bin/tarm32le/scheme -q > > Error: illegal instruction > > () > > make[10]: *** [Mf-base:375: cmacros.so] Error 1 > > make[9]: *** [Mf-base:179: allx] Error 2 > > make[8]: *** [Mf-base:196: bootstrap] Error 2 > > make[7]: *** [Makefile:22: build] Error 2 > > make[6]: *** [Makefile:20: build] Error 2 > > make[6]: Leaving directory '/home/pi/gh/racket-7.8/src/ChezScheme' > > make[5]: *** [Makefile:158: scheme-make-finish] Error 2 > > make[5]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' > > make[4]: *** [Makefile:148: scheme-make-copy] Error 2 > > make[4]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' > > make[3]: *** [Makefile:137: scheme] Error 2 > > make[3]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' > > make[2]: *** [Makefile:60: cs] Error 2 > > make[2]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' > > make[1]: *** [Makefile:90: racketcs] Error 2 > > make[1]: Leaving directory '/home/pi/gh/racket-7.8/src' > > make: *** [Makefile:53: all] Error 2 > > > > > > -- > > You received this message because you are subscribed to the Google > Groups > > "Racket U
[racket-users] ARM32 binaries for CS, or building on ARM 32
I'm wondering, does anybody have any prebuilt 32-but ARM binaries for Racket on Chez? I'm trying to run a little web-server on a raspberry pi, and I'd prefer to use the Chez version, but I can't seem to get it to build. Alternately, if anybody knows why it won't build and can help, that would help. With eiether --enable-csracket or --enable-csonly, it gets stuck compiling the forked version of ChezScheme. Surprisingly, it doesn't seem to be an out of memory error. Is the illegal instruction error because it's ARMv6 and not AArch32? ... gcc -Wpointer-arith -Wextra -Werror -Wno-implicit-fallthrough -O2 -g -O2 - Wall -DELF_FIND_BOOT_SECTION -pthread -rdynamic -o ../bin/tarm32le/scheme ../boot/tarm32le/main.o ../boot/tarm32le/libkernel.a -lm -ldl -lpthread -lrt -luuid ../zlib/libz.a ../lz4/lib/liblz4.a -pthread (cd s && make bootstrap) make allx rm -f *.tarm32le xpatch patch *.patch *.so *.covin *.asm script.all header.tmp *.html rm -rf nanopass cp -p -f ../boot/tarm32le/petite.boot ../boot/tarm32le/sbb cp -p -f ../boot/tarm32le/scheme.boot ../boot/tarm32le/scb make all echo '(reset-handler abort)'\ '(base-exception-handler (lambda (c) (fresh-line) (display-condition c) (newline) (reset)))'\ '(keyboard-interrupt-handler (lambda () (display "interrupted---aborting\n") (reset)))'\ '(optimize-level 3)'\ '(debug-level 0)'\ '(commonization-level (commonization-level))'\ '(compile-compressed #t)'\ '(compress-format (compress-format))'\ '(compress-level (compress-level))'\ '(generate-inspector-information #f)'\ '(subset-mode (quote system))'\ '(compile-file "cmacros.ss" "cmacros.so")'\ | ../bin/tarm32le/scheme -q Error: illegal instruction () make[10]: *** [Mf-base:375: cmacros.so] Error 1 make[9]: *** [Mf-base:179: allx] Error 2 make[8]: *** [Mf-base:196: bootstrap] Error 2 make[7]: *** [Makefile:22: build] Error 2 make[6]: *** [Makefile:20: build] Error 2 make[6]: Leaving directory '/home/pi/gh/racket-7.8/src/ChezScheme' make[5]: *** [Makefile:158: scheme-make-finish] Error 2 make[5]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' make[4]: *** [Makefile:148: scheme-make-copy] Error 2 make[4]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' make[3]: *** [Makefile:137: scheme] Error 2 make[3]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' make[2]: *** [Makefile:60: cs] Error 2 make[2]: Leaving directory '/home/pi/gh/racket-7.8/src/cs/c' make[1]: *** [Makefile:90: racketcs] Error 2 make[1]: Leaving directory '/home/pi/gh/racket-7.8/src' make: *** [Makefile:53: all] Error 2 -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/9b0c4921-2155-4f63-bb79-a6b9ea058ef6o%40googlegroups.com.
Re: [racket-users] Change the order of bibliography entries in Scribble?
Looks like that changes the order the citations are listed at the point of citation, but not in the generated bibliography at the end of the document? Unless I'm missing something obvious. Either way, thanks! On Thu, Mar 7, 2019 at 4:36 PM Matthew Flatt wrote: > At Thu, 7 Mar 2019 15:06:30 -0800 (PST), Joey Eremondi wrote: > > I'm using Scribble and Frog to automatically generate a publications > list > > from a BibTex file. The problem is, right now I get the same order > > regardless of what order I call ~cite: sorted by year, oldest to newest. > > I'd like the reverse of this, with newest at the top. Is it possible to > > change the order of the generated bibliography, to either match the > order I > > call ~cite in, or to automatically sort by date (in reverse?) > > You can supply `#:sort? #f` as an argument to a `~cite` to use the > order that you supply. There's not currently a way to change the > automatic sort order. > > -- > You received this message because you are subscribed to a topic in the > Google Groups "Racket Users" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/racket-users/4uIjaC1alNU/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Change the order of bibliography entries in Scribble?
I'm using Scribble and Frog to automatically generate a publications list from a BibTex file. The problem is, right now I get the same order regardless of what order I call ~cite: sorted by year, oldest to newest. I'd like the reverse of this, with newest at the top. Is it possible to change the order of the generated bibliography, to either match the order I call ~cite in, or to automatically sort by date (in reverse?) Thanks! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Examples of #:inv in Redex?
I'm wondering, are there any good examples out there of using #:inv with Redex-judgments? Particularly with asserting that some other judgment holds on the output. For example, I've got: #:contract (SomeJudgment Gamma tt gv gU) #:inv ,(judgment-holds (SomeOtherJudgment gv gU)) The problem I'm having right now is that, if I unquote gv and gU in the invariant, it says they're unbound variables. But if I quote them, it uses the literal terms (term gv) and (term gU), that is, it's not properly binding/substituting gv and gU when it's evaluating the contract. If I add a (begin (println (term gv) ... ) to the contract, it prints 'gv, confirming that the substitution isn't happening. Am I using this wrong? Are there examples of its proper usage, or is this just a mostly-unused feature in Redex? Thanks for all the Redex help! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Is there a way to fully expand and evaluate a syntax object at compile-time? (Redex compile-time typechecks)
As part of my ongoing attempt to turn my Redex model into a #lang, I'm wondering, is there a way to fully expand and evaluate a syntax object at compile-time? I'm trying to get compile-time typechecking working. Here's what I have: * My Redex model uses names like TermLam, TermApp etc. * I've defined lambda and #%app so that the user can write normal programs that are translated into Redex terms. * I've done (require (for/syntax redex/reduction-semantics "my-redex-model.rkt")), so that I have access to my Redex model at compile time When the user writes a term (using lambda and #%app macros), I need to take the syntax object I'd tried using local-expand and syntax->datum, but I think it's expanding too far, i.e. it's giving "(#%expression (let-values () (let-values (((ws1) (#%expression ..." redex doesn't know how to interpret as a term. Is there a way to do this? Or am I trying to push redex farther than intended? Thanks! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Matching against alpha-equivalence classes in Redex?
I'm modelling dependent types in redex, and I've got a rule that looks like this: [ (WellFormed (EnvExt x gU Gamma)) (Check (EnvExt x gU Gamma) gu gV) --- "CheckLamPi" (Check Gamma (CanonicalLam x gu) (CanonicalPi x gU gV))] CanonicalLam and CanonicalPi each bind x inside gu and gV respectively. The problem is, elsewhere in my model I have a type normalization judgment, and when it normalizes the CanonicalPi type, it binds a fresh variable, not the original variable that was given. This causes the "CheckLamPi" rule to never be called in typechecking, since it no longer What I really want is to treat terms as alpha equivalence classes, i.e. to write something like the above, and have it implicitly be implemented as something like this: [ (fresh z) (WellFormed (EnvExt z gU Gamma)) (Check (EnvExt x gU Gamma) (subst z x gu) (subst z y gV) ) --- "CheckLamPi" (Check Gamma (CanonicalLam x gu) (CanonicalPi y gU gV))] That is, I want the pattern matching not to check if the term and type bind literally the same variable, but to alpha-rename them to something that binds the same name. Do I have to write a rule that explicitly does this substitution? Or is there a way to tell Redex that I mean the second form when I write the first? Thanks! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Debugging Judgements in Redex?
Perfect, that did the trick, thanks! On Wednesday, January 2, 2019 at 7:52:40 PM UTC-8, Robby Findler wrote: > > Did you try using `current-traced-metafunctions` ? It is poorly named, > I know. And, even worse, I see that the docs don't actually say that > it traces judgment forms too. > > Robby > > On Wed, Jan 2, 2019 at 9:18 PM Joey Eremondi > wrote: > > > > I'm wondering, is there a way to show some sort of trace for a call to > judgment-holds that returns '() or #f? > > > > I'm in a situation where a judgment that I expect to hold does not, and > it's tricky to find out by hand where it is failing. The #mode requirement > for the judgments suggests an obvious algorithm for establishing whether a > judgment holds, which I assume is what judgment-holds uses. Is there any > way to see what steps it takes, and were it fails? > > > > -- > > You received this message because you are subscribed to the Google > Groups "Racket Users" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to racket-users...@googlegroups.com . > > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Debugging Judgements in Redex?
I'm wondering, is there a way to show some sort of trace for a call to judgment-holds that returns '() or #f? I'm in a situation where a judgment that I expect to hold does not, and it's tricky to find out by hand where it is failing. The #mode requirement for the judgments suggests an obvious algorithm for establishing whether a judgment holds, which I assume is what judgment-holds uses. Is there any way to see what steps it takes, and were it fails? -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Re: Redex: making a #lang with native lambda, app, etc.
Thanks for the response! That's not quite what I want. That will quote lambdas and applications into my redex models, but I also want it to reduce them by my reduction relation. The link I posted discussed how to do that, but only when you write programs in the syntax of the model. Sorry for not being clear about the top-interaction. There's nothing specific about top-interaction, I'm having the same problem with module-begin. I'm trying to get them both to evaluate the terms using my redex model. The local-expand function in the article you give looks promising, but I'm still figuring out how exactly to use it, particularly with the list of expressions for module-begin. On Monday, December 31, 2018 at 8:47:49 PM UTC-8, Sorawee Porncharoenwase wrote: > > I'm a novice too, but here's my attempt to help. > > >> I'd like to use (define-syntax) to make lambda, #%app, etc. all expand >> into terms in my model. >> > > This works for me. Is this what you want? > > #lang racket/base > > (require redex) > > (define-language L > (term ::= > (TermLambda var term) > var > (TermApp term term))) > > (define-syntax-rule (lambda (x) b) > (term (TermLambda x b))) > > (default-language L) > > (lambda (y) y) > ;; => '(TermLambda y y) > > (term (substitute ,(lambda (y) y) y z)) > ;; => '(TermLambda z z) > > > >> But the problem I'm running into is that #%top-interaction applies (term) >> to its argument, which means that 'lambda' and other macros get quoted and >> not expanded. >> > > I don't totally understand how #%top-interaction is relevant here. It only > comes up when you use the REPL, and even then I think it shouldn't do > something like that. What are you trying to do in the REPL? And can't you > redefine #%top-interaction so that it doesn't do what you don't want it to > do? > > >> Is there a way to make sure that the macros are expanded *before* they >> are passed to term, so that (term) receives valid syntax trees for my >> model, instead of quoted lambdas and apps? >> > > See > https://lexi-lambda.github.io/blog/2018/10/06/macroexpand-anywhere-with-local-apply-transformer/. > > You can also just use the gist here: > https://gist.github.com/lexi-lambda/65d69043023b519694f50dfca2dc7d33 > > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Redex: making a #lang with native lambda, app, etc.
I've got a model for a language I'm working on in PLT Redex, but it's auto-generated by another tool (Ott). Because of this, the syntax comes out in somewhat obfuscated format: (define-language L (term ::= (TermLambda var term) var (TermApp term term) ) I've found this guide for making a #lang based on a redex model: http://docs.racket-lang.org/redex-to-lang@pcf/index.html I'd like to use (define-syntax) to make lambda, #%app, etc. all expand into terms in my model. But the problem I'm running into is that #%top-interaction applies (term) to its argument, which means that 'lambda' and other macros get quoted and not expanded. Is there a way to make sure that the macros are expanded *before* they are passed to term, so that (term) receives valid syntax trees for my model, instead of quoted lambdas and apps? I'm still pretty new to macros/metaprogramming/quasiquotation, so I might be missing something obvious. Thanks! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
