
fun project I’m working on as part of resyntax
: a #lang
for testing refactoring rules #lang resyntax/testing/refactoring-test
require: resyntax/refactoring-rule let-to-define
test: "single let binding"
--------------------
#lang racket/base
(define (f)
(let ([x 1])
1))
------------------
#lang racket/base
(define (f)
(define x 1)
1)
------------------
test: "multiple let bindings"
---------------------
#lang racket/base
(define (f)
(let ([x 1]
[y 1])
1))
---------------------
#lang racket/base
(define (f)
(define x 1)
1)
---------------------

I suppose the original purpose was to be able to deal with these #lang
lines?

That’s a really good discussion.

What maybe needs more discussion: “You Want it When? And How? And How Fast?”

Like, if it takes a few seconds for background expansion to do check-syntax, people mostly seem OK with that.

But if they hit ENTER or TAB and nothing happens for a few seconds, maybe not?

Also it’s easy for an API that uses “call me” to work when the tool is DrRacket, but how does it work when the tool is a command-line utility or vim or emacs or vscode.

So I could be wrong but my hunch is this will turn out to be more like building documentation, in terms of when Racket code is evaluated, and how and where information is made available.

All this might be moot for a non-sexp syntax. Maybe macros get indented like functions, end of story. Or maybe indentation isn’t style, it’s information, because the syntax is off-side rule or whatever. So idk.

I think we also need a hook to restart the backend server and re-check the currently opened buffers after racket-mode-start-faster

@capfredf That’s an interesting point about restarting the backend server. Probably racket-mode-start-faster
should call racket-mode-stop-backend
before doing the raco make
. And after, either call racket-mode-start-backend
, or do nothing and let it be auto-started on-demand when some command needs it.
But why re-check all currently opened buffers? The annotations are sitting in the buffer (as text properties). I think they would still be useful and valid. OK, maybe not if e.g. you wanted something like online-check-syntax
logger messages to be from the just-updated version of Racket.

Yes, it would not be necessary when I was not modifying (typed) racket source code. But that is not the case most of time for me.

Let’s say I’ve got a (python, in this case) template like this: (parameterize ([sandbox-output 'string])
(let* ([code '(begin
${code} ; newline here in case code ends in a line comment
)]
[e (make-evaluator 'racket code)])
body...))
where I’m going to put student code in the ${code}
position, and it comes from a web-request.
Is there a way to make sure that ${code}
is syntactically valid on its own, or otherwise sanitize it? I’m in Python, and have code
as a string, but I can shell out to racket or whatever.
Simple injection attack: code=')] [injection (displayln "hello")] [dummy (list'
. More elaborate escapes are probably possible with enough closing delimiters, code, and either open delimiters or #;(
forms.

You can try to read
the code first maybe, so at least it would be valid s-expr

Not sure what you mean by “I’m in Python”. Is the student code in Racket then?

Yeah, student code is a python string; I’m building code to run in a subprocess (basically a sandbox for the student code, with some unittests).
Are you thinking something like (read '${code})
? That might well work.

Probably: (with-input-from-string student-code-string read)

But if the student code is python code that won’t help you much

unless you have a python-read
function

There must be a python-read
in the implementation of #lang python
.

No, student code is racket, but the program is python executing racket. Confusing, I know. I’m realizing that might suffer from the same issue; I could theoretically set code='end string" (exit 0) "'
and then (with-input-from-string "${code}" (read))
would become (with-input-from-string "end string" (exit 0) "" (read))
… maybe I can escape quotes, though, and that’s a simpler problem.

How about a here-string ?

Yeah so recap on context: I’m building a string of racket code in python. How to safely inject student code?

Ooh here-string is clever. It’s all literal til the delimiter, right? As long as the students never figure out the delimiter…

Indeed.

Or I add spaces to the front of each line; then the delimiter (even if present) is not able to end the here-string, right?

An md5 of some phrase might be just as easy to use.

(as an unguesable here-string-delimiter)

thanks folks, this gives me some things to try. will report back

How about writing the student code to a temp file, and have it read as a string or with python-read from racket? The code wouldn’t be inside your own racket file then.

You can even turn it into a module (or require that students produce a module), so you can do properly dynamic-require

You can just pass the string to make-evaluator
, and it will raise an error if the string does not contain a well-formed program. > (define e (make-evaluator 'racket "(define x 1) (+ x 2)")) ;; okay
> (define e (make-evaluator 'racket "(define x 1) (+ x 2) (bad "))
; program:1:21: read-syntax: expected a `)` to close `(` [,bt for context]

I thought about using a file, but I wasn’t entirely sure how to glue the pieces together. I can’t just pass it directly to make-evaluator
because we also want code as quoted-data, e.g., to check that code calls a certain function :disappointed:

The here-string so far seems to be fine. The previous syntax I showed for an injection doesn’t work inside the here-string. Breaking out of the here-string early means the regular racket reader catches it. As long as I prevent closing the here-string early, you can’t get out and do something like 'valid
DELIMITER
(exit 0) #<<DELIMITER
'more-valid
and cause an early exit. And I think this is feasible by inserting spaces after all newlines.

if you put the code into a file, you can evaluate it with dynamic-require, but you can also read-it with read
. You just need to make sure you enable reading #lang lines

@samth Issue; code not yet merged: https://github.com/greghendershott/racket-mode/issues/517


Decided to help out and download the new Windows build per John’s instructions. Can’t be the only one. 2.5 KB/sec!

:disappointed:

On the bright side, the three other links download with the whopping speed of 200 KB/sec :slightly_smiling_face:

Ah! The trick was to pause and resume. Not used to Windows…

I downloaded both versions of the 64 bit build and they downloaded at about 1MB /sec , which is the capacity of my internet connection…

… using Windows and the Edge browser…

The lang blocks just get turned into strings for now. The main reason I wrote this is so I wouldn’t have to write long multi-line string literals with semantically-meaningful indentation in my test cases :sweat_smile:

Hey, you guys beat me, I haven’t even posted the request on slack yet!

Okay, here’s the request.

Specifically, the release candidates for racket 8.0 for Windows are currently available at these URLs
https://mirror.racket-lang.org/installers/8.0/racket-8.0-x86_64-win32.exe https://mirror.racket-lang.org/installers/8.0/racket-8.0-x86_64-win32-bc.exe https://mirror.racket-lang.org/installers/8.0/racket-8.0-i386-win32.exe https://mirror.racket-lang.org/installers/8.0/racket-8.0-i386-win32-bc.exe
Unfortunately, Microsoft’s SmartScreen currently flags these binaries as “blocked because it could harm your device” when downloading using Edge, and possibly malicious at installation time when downloaded using another browser.
Our research suggests that the solution to this is … just to download it a lot. Also, to download it using Edge, and use the three-dots menu to report it as a safe website. We’ve submitted the file to Microsoft, and they cheerfully reported that the file would no longer be flagged. Unfortunately, this is clearly not the case.
So, we’re asking for help of two different kinds.
1) If you use Windows, please take a minute to download and install the binary from one of these URLs. Plus, you get a special PREVIEW copy of 8.0, you lucky duck!
If you get the chance to do this, we’d also be grateful if you would fill out this five-multiple-choice google form, so we have some idea of how many people are actually doing this and whether people are still seeing the smartscreen warnings.
2) If you use Windows and you have experience that would suggest that we’re somehow misunderstanding this situation, we’d love to hear about it.
Many thanks!
John Clements

Testing now, but this is a new setting (screenshot) with the latest windows 10 updated that might be affecting people, as the default was changed out from everyone to the most strict settings:

With it set to “Anywhere”, I was able to download and install out-of-the-box with only the typical “This program isn’t known by Microsoft” blue popup (read: it isn’t a signed app through the MSFT app store).

It ran just fine, too.

Is this meant to be a temporary solution? Do we need to do this all over again for 8.1? Does SmartScreen use domain name or exact URL or binary checksum? Does this mean (Minimal|regular) Racket (CS|BC) need to be all downloaded?

From what I understand it has to do with the reputation (as judged by some opaque Microsoft algorithm) of the certificate used to sign the executables. Presumably once that reputation is established we won’t have to do it again as long as the same cert is used

Looks like the cert used to sign these is only a few days old and is good until Feb 2023. I don’t know if there’s a mechanism to have your “reputation” carry over to a new one.

We’re also likely to pursue getting an EV certificate

Maybe it would also be simpler to have a tiny installer that never changes and downloads rest of Racket once you run it.

I guess EV would obviate the need for that though.

Wouldn’t that be equivalent to using non-Edge browsers to download the executable file?

It kinda doesn’t matter what browser you use…if you use another browser you will just get the same “SmartScreen blocked this” message when you try and run the installer. there is a “run anyway” option but it’s hidden behind a “details…” link

I think self-updating would be good, but “never changes” seems hard to achieve

Hi, Quick Question, in Typed Racket, any way to add constraint on All
type constructor. (define-type Foo (U Type-A Type-B))
(: bar : (All (T in Foo) T -> T))
;; T can be instantiated (only) as Type-A, Type-B

(: bar (-> Foo Foo))
code like this actually leads to more than two types, like (-> Type-A Type-B)

You can use Intersection
, I think.

If T in Foo
means T <: Foo
, then TR doesn’t support bounded quantifications


@capfredf yes, I haven’t found it too, but any work around about this?

You can try intersection types, but I am not sure if that will work for your case

Can you give a more concrete example?

no specific problems, actually I just explore to use union types and its subtyping to simulate Haskell’s typeclass

Yes I tried Intersection, it add constraint on the other side, not really solve this problem (define-type Foo (U Type-A Type-O Type-B))
(define-type Bar (U Type-A Type-O Type-C))
(: fun (-> (Intersection Foo Bar) (Intersection Foo Bar)))
;; it accpets (-> Type-A Type-O)

I meant something like:
(define-type Foo (U Symbol Number))
(: bar : (All (T) (Intersection T Foo) -> T))
(define (bar x)
x)

awesome, this looks a great solution

@bfowke has joined the channel

@luke has joined the channel

so its done on everything but windows?

ahh nevermind “Preview” copy. what are the blocking issues from final ?

question, how come the 2021–02–10 snapshot CS is 126 MB and the one you linked is 173MB? curious as to what is added

I found an old issue that is very close. It’s likely that some old homebrew formula did not install Racket correctly. https://github.com/racket/racket/issues/3089