regarding documentation, I really miss some tooling to generate scribble stubs for provided procedures. Given that contracts are provided, would that be hard to do? I am also currently documenting a new package and Scribble is a real barrier for me. I feels like learning a new language

You could try <https://docs.racket-lang.org/scribble/srcdoc.html?q=srcdoc|In-Source Documentation> .

Not to discourage the in-source documentation, but from my experience, the setup is even more difficult than regular Scribble.

Sandbox is only going to bring you safety (restricted access to ports, max memory allocation, etc.), but is not going to be faster. Plus your primitives don’t have access to these objects so you don’t really need sandbox. Except maybe if you want to automatically kill long-running programs or memory hungry ones, in which case you can use with-limits, but be warned that it defeats errortrace which makes debugging harder (so it’s best to not use it when debugging).

I completely agree that documentation should be more straightforward than it currently is. [Throwback Tuesday] A looooong time ago, when I was just getting back to PLT Scheme, my main issue was precisely the lack of easy in-source documentation, so I wrote <https://planet.racket-lang.org/package-source/orseau/lazy-doc.plt/1/1/planet-docs/manual/index.html|my first package> to fix this (in-source scribble didn’t even exist at the time I think? Or at least I didn’t know about it). Not very long afterwards, I considered it was very non-rackety and rather bad style—though probably everyone else who had read the docs of the package had considered it bad style much earlier.

I’ll admit that in-source documentation is not as convenient as I’d hoped. Considering Scribble in general, I’ve found that it’s awkward to document anything other than what the standard def... forms cover. Also, documenting a #lang that has different syntax and constructs than Racket looks rather difficult.

Has Scribble been used for anything other than documenting Racket/reimplementations of Racket/ DSLs made in Racket?

https://docs.racket-lang.org/brag/index.html?q=brag\|brag is an example of a #lang with non-s-expr syntax that is documented with Scribble. Since it is a specialized DSL and is easily explained with examples, the documentation isn’t bothered too much by the difference from Racket.

Hmm, I wonder how hard literate programming would be with other languages (especially compiled), like C++ or something similar.

Sure. Ages ago I used it to write a whole teaching book for PHP :sweat_smile: I’m also using it do some kind of literate programming: Initially I was using google docs, but as I kept changing numbers I had to rewrite most of the doc, likely leaving mistakes here and there, so I switched to scribble and would certainly not go back. (however, I’m using lots of utf–8 symbols, and even xelatex has issues with this, so I’m first generating html then html->pdf via an external renderer)

Also I’m pretty sure some people use scribble to generate their web pages (even without frog)

Confused about convention of non-terminals identifiers in Redex: In Ott, I can write the following A, B, C, D ::= \| Int \| Top \| A -> B where C, D can be used in later rules/judgements. In Redex, it seems that people tend to write code like (τ := Int Top (τ -> τ) and in later rules, use τ_1, τ_2 in define-judgment-form to differentiate identical terms. Can I keep my style in Ott and write Redex code like this? (define-language AppL (e ::= n ;; int x ;; variable (λ x e) ;; abstraction (e e) ;; application (x τ) ;; annotation ) (n ::= number) (A B C D::= Int ;; int type Top ;; top type (A → B) ;; function type ) (x ::= variable-not-otherwise-mentioned)) (define-judgment-form AppL #:mode (subtype I O) #:contract (subtype A B) [--------------- sub_int (subtype Int Int)] [--------------- sub_top (subtype A Top)] [(subtype C A) (subtype B D) ------------------------ sub_arrow (subtype (A → B) (C → D))]) If I run (judgment-holds (subtype Int Int)) and Racket gives me error the following subtype: judgment values do not match its contract (or invariant); contract: (subtype A B) values: (subtype Int Top) I must misunderstand something, such as mis-use name in #:contract or name in judgements Can someone help me with this?

I’ve used it to generate a bunch of web pages, even some that have nothing to do with Racket. And people write papers with it, and books.

It’s the D::=. You need a space there, otherwise it’s a single identifier and means something different than you intended.

You’ll run into another problem after that, which is that your subtype relation has the mode I O, which is saying “given a type A, compute all types B that are a subtype of A.” That makes your sub_arrow rule problematic because it uses an output of the conclusion as an input in one of the premises. You probably want an I I mode, which says: “given two type A and B, determine if A is a subtype of B.”

@dvanhorn thanks for your reply, that’s very helpful! II mode work as intended. I need to further read some docs of mode.

Judgments in Redex are defined algorithmically, so think of each judgment as a a function from inputs to sets of outputs. The mode specifies which positions are inputs and which are outputs. If a judgment has only inputs, you can think of it as a function that consumes those inputs and produce true or false for whether the inputs are in the relation specified by the judgment. The rules of a judgment have to be “well-moded” which is essentially saying that outputs in the conclusion have to be computed from inputs to the conclusion or outputs of the premises.

This is unlike some other relational programming languages, e.g. Prolog, where you can define a relation logically without regard to how it is computed and the system will do proof search. That’s not what’s happening here: you’re writing a functional program from inputs to (sets of) outputs.

@dvanhorn Thanks for the explanation! I see your point, declarative rules is hard to implement and Redex favours the algorithmic one. About the notion/terminology of mode, input and output, I’m not sure what Redex mean is the same as the one I know: If you are familiar with bidirectional type checking, there’s a so-called checked-mode and inference-mode, and we should carefully select which term is input and which term is output in the rules when you implement it.

btw, actually I didn’t any redex examples adopt II mode, don’t know why

There’s a thing called define-relation that makes a judgment where every position is an input. If you look at the docs for it, the example given is a subtyping relation like the one you wrote. :)

I think the connection to bidirectional typing is appropriate. In checking mode, you are given a type (I) and expression (I) and check whether the expression has that type. In inference mode, you are given an expression (I) and synthesize its type (O). A good exercise would be to model a simple bidirectional type system in Redex. I think it’s well-suited for that.

thanks, really appreciate it!

I am missing something… ; FAILURE ; /Users/soegaard/Dropbox/GitHub/racket-cas/racket-cas/new-format.rkt:1031:4 name: check-equal? location: new-format.rkt:1031:4 actual: '("0" "1" "−1" "2" "−2" "1/2" "−1/2" "1.5" "-1.5") expected: '("0" "1" "−1" "2" "−2" "1/2" "−1/2" "1.5" "−1.5")

maybe some weird unicode character?

Yes. Found the suspect: new-format.rkt/test> (for/list ([a ’(“0” “1” "−1" “2” "−2" “1/2” "−1/2" “1.5” "–1.5")] [e ’(“0” “1” "−1" “2” "−2" “1/2” "−1/2" “1.5” "−1.5")]) (list a e (equal? a e)))

’((“0” “0” #t) (“1” “1” #t) ("−1" "−1" #t) (“2” “2” #t) ("−2" "−2" #t) (“1/2” “1/2” #t) ("−1/2" "−1/2" #t) (“1.5” “1.5” #t) ("–1.5" "−1.5" #f))

One minus is shorter than the other.

Ah! I remember now. When outputting in NSpire-format, a minus sign is different from a subtraction minus. So the test is correct - it caught an error.

Oh! It’s easier to spot in slack. The font in Emacs displayed the two characters as the same glyph.

For my font in Emacs (for some months now I’ve been having an affair with old school “IBM Plex Mono”) it’s about as obvious as in Slack. But even with that, I could still imagine staring at that for waaaay too long without seeing it.

This seems like a variation, for failing tests, on the rule that the longer it takes to debug something, the simpler the answer will turn out to be. :smile: At least I’ve starred in that drama far too many times. I’m sure many more still to come.

I am rewriting an sexp to infix formatter for algebraic expressions. The code of the original formatter was very pretty - but only handled normalized expressions. Then I got the idea to extend it - and added special case after special case. At the end I spent way to much time to fix corner cases in the old code - hence the rewrite.

I am getting some deja vus however :slightly_smiling_face:.

And boy am I glad I wrote tests for the original implementation.

I’ve been looking at whether it’s possible for a function to know the srcloc of a call site — “I was called from /path/to/foo.rkt:1:2:3:4”. I’ve concluded that it’s not possible. (Not without something like a custom #%app in the module’s call site arranging for this srcloc to be tucked away in a continuation-mark or some such mechanism. And not without a custom load- or eval-handler.) Knowing the “context” from cms->context, sure, but that’s a wide span around the actual site. Does that seem correct, that it’s not generally possible?

Related: I double-checked that contract blame doesn’t somehow have this ability (I expected not, but just as a sanity-check.) It doesn’t AFICT: It’s always “blaming <file>”, a file in general. But I noticed something weird. With contract-out, the using i.e. calling file is blamed. With define/contract, the defining file is blamed. Is that known and as-expected?

E.g. assuming contract-use.rkt is #lang racket (require "contract-def.rkt") (foo "a")

With contract-def.rkt as #lang racket (provide (contract-out [foo (-> number? number?)])) (define (foo x) x) The blame line is blaming: /path/to/contract-use.rkt

But with contract-def.rkt as #lang racket (provide foo) (define/contract (foo x) (-> number? number?) x) The blame line is blaming: /path/to/contract-def.rkt. i.e. You can’t tell where to look for the problematic call.

I realize contract-out is generally recommended over define/contract, for various reasons.

I just didn’t remember “non-useful blame” as one of the reasons, so I was surprised.

That’s correct: The only information available is in the continuation as reported by continuation-mark-set->context.

Thanks for confirming!

I’ve been wanting exactly this kind of information, too

I’ve found this pretty annoying for years. And I think if you try contract-out with ->i, it’s back to non-useful blame again, because (if I recall correctly) contract-out has special support for -> and ->* but not ->i.

Somehow my programs full of contract-out and ->i do end up having useful highlighting of contract-violating call sites in DrRacket, but I rarely use DrRacket and don’t think I can infer that location information from the error messages I get with the racket executable.

I think even define/contract programs have useful call site highlighting in DrRacket.