tnelson / forge Goto Github PK

The following file:

sig A {}
sig B {}
run {} for 3 but 3 A, 3 B

produces this error with no highlight or line number. This happens when pasting in old models from Alloy for update, since Alloy supported adjusting default bounds.

I'm not proposing that Forge support adjusting default bounds necessarily, just that the error be improved.

Could this be an option?
Even if not, better to support the in-class syntax.

Alloy has a "fast, medium, slow" menu for core extraction. This is distinct from core granularity.
I believe this controls which strategy is used (HybridStrategy, RCEStrategy, etc.)
It's unclear which we're using right now -- probably the fast version.

check-ex-spec needs to create usage logs so that we can study how students use it

Example research questions:

• do students use check-ex-spec at all? early? late?
• how does student code change between check-ex-spec runs?

Jack suggests we collect simple data. Just get the student code; structure it later. With that in mind here's a database idea:

• current source code (string)
• wheat/chaff output (string, or S-expression)
• current filename
• timestamp
• student id (the prefix from a brown.edu email address --- ask for at #lang line?)
• submission number (natural number --- incremented after each run, useful to detect missing data)

Thomas has much richer data going at the logging branch, though. We'll have to meet and figure out what's best.

To collect data, Jack suggests using a Google Cloud function & posting to a SQL database. I have access to a Cloud Platform account and can write a cloud function there (console.cloud.google.com).

Here's a SQL link:
https://cloud.google.com/sql/docs/mysql/connect-functions

from Piazza @119:

make-directory: cannot make directory
  path: /Users/sarah/.config/forge/
  system error: Permission denied; errno=13

Lets do two things:

1. try to set permissions on the directory that basedir gives in forge/logging/logging.rkt
2. catch the exception, print a warning, and turn off logging if it happens

The expander invokes many macros defined in sigs.rkt, such as pred, fun, sig, etc.
Right now, syntax locations are generally not preserved by these, EXCEPT for the "pred" macro in sigs.rkt.
This means some errors will possibly give source location from expander.rkt. I only fixed the pred macro, since it was producing malformed errors if I (e.g.) defined a function as a predicate.

See my commit here for a possibly useful pattern: 7990881
Instead of the (crossed out) commit above, which was buggy, see this commit: 5217b1b
In particular, the issue can be avoided by simply using quasisyntax/loc to embed a syntax/loc (thus setting the correct location in the subexpression).

Hi, both my friend and I have been having in issue in Forge where the right bracket symbol doesn't work. Similarly to other issues in the past, erasing part of the "forge" declaration in "#lang forge" fixed it.

Right now there's no unsat-core highlighting feature in Forge. This means that users have to look in the REPL for the core -- and it's not displayed in a very readable way.

Ideally, we'd be highlighting regions of the editor like Alloy does.
(Tim did some initial experiments on highlighting multiple different regions via a tool -- see the tool-experiment branch.)

We want to be able to require just the spec (sigs, relations, preds, functions) from a given forge program without executing the run statements.

subset sigs are not currently supported in Forge, but appear in many Electrum demos.

It would be nice if the Navbar used links instead of on clicks. This also effects accessibility.

#lang forge

aRun : run {}

sig A {}

Then, referring to A in the evaluator during aRun causes PardinusCli to shutdown with

No definition found for rS. (line 1, pos 10):
BasicParseError (line 1, pos 10):
[error] [blank] No definition found for rS. (line 1, pos 10):
[error] [blank] BasicParseError (line 1, pos 10):
[error] [blank] No definition found for rS. (line 1, pos 10):
[error] [blank] BasicParseError (line 1, pos 10):
#<eof>

sig Atom {edges: set Atom}

run {} for exactly 0 Atom

Doesn't fail if run for exactly 1 Atom or without the edges set.

When trying to run, received

\Roaming\Racket\7.0\pkgs\forge\sigs.rkt:424:9: error writing to stream port
system error: The pipe is being closed.; errid=232

The 'func break when applied to a relation from a sig to itself causes an unsound relation break. It enforces that some node can only point to itself, if anything.

#lang forge/core

(sig A)
(relation r (A A) #:is func)

(pred irreflexive
  (no (& r iden)))

(test func-bug ; fails
      #:preds [irreflexive]
      #:scope ([A 3 3])
      #:expect sat)

The above code produces the following KKCLI bounds:

(r:A [{(16) (17) (18)} :: {(16) (17) (18)}])
(r:r [(-> none none) :: {(16 16) (17 16) (17 17) (17 18) (18 16) (18 17) (18 18)}])

E.g.,

******************** testing ./forge-core/examples/booleanLogic.rkt
uncaught exception: "Upper bound too large for given BitWidth; Sig: #(struct:Sig Formula (relation 1 "Formula" (Formula) univ) #f #t #f (Var Not And Or)), Upper-bound: 8, Max-int: 7"

Right now we're always encoding bounds numerically, even when we don't have to.

Change check-ex-spec so that it doesn't try to download files during background expansion.

When everything's fixed, we should be able to open a new file in a new directory and see no red error messages in the editor.

Example file:

#lang forge/check-ex-spec "forge2/undirected_tree"

Current error output:

make-directory: forbidden (write) access to compiled

EDIT: more errors

tcp-connect: forbidden client access to raw.githubusercontent.com:443

../code/racket/fork/extra-pkgs/Forge/forge/check-ex-spec/lang/reader.rkt:25:26: hash-ref: contract violation
  expected: hash?
  given: 404
  argument position: 1st
  other arguments...:

Make sure that students save their code before running, either by:

• automatically saving when "Run" gets clicked
• or refusing to run unsaved definitions

(Because if the file isn't saved, the snapshots that we try to collect based on the filename are outdated.)

Add syntax semantic highlighting to Forge for VSCode users. Make sure that errors highlight the source.

EDIT: after finding the ErrorLens package today (2021-12-18), I'm not sure a semantic highlighter is needed. Maybe we can get by with a plugin that looks at recent diagnostics.

EDIT 2: well, we need some way of making those diagnostics. A language server seems like the most straightforward way. Though, maybe there's a simpler way to get diagnostics from the terminal.

How?

• Port the forge grammar from Brag to TextMate (done?)
• Make a language server
• ???

Resources

VSCode semantic guide: https://code.visualstudio.com/api/language-extensions/semantic-highlight-guide

VSCode languages API, especially getDiagnostics https://code.visualstudio.com/api/references/vscode-api#languages

VSCode extension samples https://github.com/microsoft/vscode-extension-samples

VSCode Error Lens package: https://marketplace.visualstudio.com/items?itemName=usernamehw.errorlens

VSCode syntax guide: https://code.visualstudio.com/api/language-extensions/syntax-highlight-guide

Example: Magic Racket https://github.com/Eugleo/magic-racket
Example: DrRacket Colors https://bitbucket.org/Dima4ka/vs-code-drracket-colorizer/src/master/

Prototype: forge-0.0.3.vsix.zip
More Prototypes: https://drive.google.com/drive/u/1/folders/1cuNtlRwgcX2Rr7gGsUoYQPKwXBilDMHb

When you have a function application followed by a join, it has the wrong precedence, so

sing[1].succ

throws an error, but if we add parens, it doesn't:

(sing[1]).succ

Ideally the precedence would be such that we didn't need to do that. (might be a box join sideeffect?)

If-then-else formulas are supported via sugar.
Expressions require a new AST node type.

It's super easy to accidentally write a Forge constraint involving join that's always empty. Maybe you forget which side of a relation has a certain type.

sig A {r: B->C}
sig B {}
sig C {}

pred test {
-- always empty
all x : r.r | ...
}

Alloy had the ability to give a warning when this could be detected statically. I have made SO MANY ERRORS this way, and I students have as well. Let's bring back this warning message (and any others that seem appropriate?)

Just curious: why don't we use the xml collection to convert Racket value to XML string? It's easier to manipulate xexpr, less error-prone, and probably more efficient than using string-append (which could theoretically take quadratic time in the size of the datum).

(equal? true true)
#f

The nodeinfo field should be ignored re: structural equality.

To see what needs to be done, view:
https://docs.racket-lang.org/guide/define-struct.html
Section 5.5. Structure Comparisons.

This essentially amounts to re-defining equals() and hashCode() for Racket structs, ala what we've all had to do in other languages before.

I recently had a problem where I forgot to enable temporal mode but was using its features, making my runs unsat. It could be helpful to have an error if trying to use temporal mode-specific syntax without enabling it!

Hi,

So far forge has not been able to run anything on my laptop - when I click "run" on any file, no browser window pops up and it gives the error "Kodkod CLI shut down unexpectedly!". I have updated forge to the latest version, but nothing has changed.

Dr.Racket version: 7.5

Java version: java version "1.6.0_65" , Java(TM) SE Runtime Environment (build 1.6.0_65-b14-468), Java HotSpot(TM) 64-Bit Server VM (build 20.65-b04-468, mixed mode)

OS: macOS High Sierra 10.13.6, 64 bit

spec: everything

Thank you!

Right now adding a new option requires changes in several places:

• the Options struct defn
• the init-options define
• state-set-option (in 2 places!)
• get-option

We did this for 2 reasons:

• I couldn't figure out how to cleanly update struct values without knowing the field name at compile time (maybe switching to macros could fix this?)
• It enables some type-checking so students who try to use an unknown field, or give a wildly wrong value, will receive error messages rather than silent failure.

The errors still aren't great because we don't catalogue the actual set of valid values. E.g., logtranslation can meaningfully be 0, 1, or 2 -- but not 100.

Fixing this probably means creating a custodian that kills all runs on termination.

(From Thomas from Slack) I found a sample program that causes the logging to get out of sync:

#lang forge/check-ex-spec "forge2/spanning_tree" "[email protected]"
test expect {
    alwaysSat : {} is sat
}

Output:

#<void>
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/summary-forge2-spanning_tree.json
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/wheats-0_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/wheats-0_rkt.dep
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-0_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-0_rkt.dep
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-1_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-1_rkt.dep
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-2_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-2_rkt.dep
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-3_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-3_rkt.dep
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-4_rkt.zo
download-file link: https://raw.githubusercontent.com/tdelv/lfs-2021-check-ex-spec/master/forge2/spanning_tree/chaffs-4_rkt.dep
LOGGING: Found 1 logs; 1 valid.
(http-response 201 '#hash(("Content-Length" . "25") ("Server" . "Google Frontend") ("X-Cloud-Trace-Context" . "6e215a93deef0b1249fac77bed6a0a4f") ("Alt-Svc" . "h3-29=\":443\"; ma=2592000,h3-T051=\":443\"; ma=2592000,h3-Q050=\":443\"; ma=2592000,h3-Q046=\":443\"; ma=2592000,h3-Q043=\":443\"; ma=2592000,quic=\":443\"; ma=2592000; v=\"46,43\"") ("Function-Execution-Id" . "0lar4ewdzs3a") ("Date" . "Sat, 06 Feb 2021 01:32:19 GMT")) "Successfully logged data.")
#t
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 59); Solving (ms): (time-solving 3)
#<void>
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 46); Solving (ms): (time-solving 4)
#<void>
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 47); Solving (ms): (time-solving 3)
#<void>
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 47); Solving (ms): (time-solving 3)
#<void>
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 47); Solving (ms): (time-solving 3)
#<void>
#vars: (size-variables 337); #primary: (size-primary 52); #clauses: (size-clauses 497)
Transl (ms): (time-translation 46); Solving (ms): (time-solving 3)
Missed chaff 0.
Missed chaff 1.
Missed chaff 2.
Missed chaff 3.
Missed chaff 4.
LOGGING: Found 1 logs; 1 valid.
(http-response 201 '#hash(("Content-Length" . "52") ("Server" . "Google Frontend") ("X-Cloud-Trace-Context" . "d0b5d4b80619a4a1aef063971ab24553") ("Alt-Svc" . "h3-29=\":443\"; ma=2592000,h3-T051=\":443\"; ma=2592000,h3-Q050=\":443\"; ma=2592000,h3-Q046=\":443\"; ma=2592000,h3-Q043=\":443\"; ma=2592000,quic=\":443\"; ma=2592000; v=\"46,43\"") ("Function-Execution-Id" . "fbl29ltni103") ("Date" . "Sat, 06 Feb 2021 01:32:22 GMT")) "There was an error, but logs were saved to database.")
#t

The output suggests that Racket is not waiting for a response from the server, and is instead continuing with it's execution (I say this because the 1 logged file in the first log print is an execution log, which came from the current execution, and all of the download process plus execution logging happens after the flush log.)

The following code does not produce the correct instance:

#lang forge

sig Node {
    g: set Node
}

inst Test {
    Node = (N1 + N2 + N3)
    g = (Node->Node) - iden
}

run {} for Test

Instead it produces this instance:

Which is incorrect because it includes self-edges which should have been removed by the line g = (Node->Node) - iden

Clicking through too fast causes display bugs and the animations generally get in the way.

For example, in the above image, Node7 is connected to Node2 (confirmed using the evaluator), but the graphic is wrong. This was caused by rapidly clicking through.

Ideally the option wouldn't need to be set each time a new instance is opened.

This includes considering how instances play with Electrum's variable relations.

TN: I'm not sure where these are coming from, both in terms of printf/display/etc. location and in terms of stdout/stderr from Kodkod.

I also wonder if we could send over more structured info with the solution. It feels like this should be a 3rd component of the result (besides sat/unsat and instance/core).

Should add anntations on projection for relations that have one column left.

The Forge logs store anonymized filenames. The current anonymization, though, is probably more likely to have a "hash" collision.

Here's what currently happens in forge/logging/logging.rkt

1. get an absolute path from the student
2. use sha256 to hash the full path
3. get the filename from the full path
4. use format to save the filename + hash to a string

The problem is that sha256 returns a bytes? and the default conversions from bytes to string can lose information. Any byte that's outside the UTF-8 range gets replaced with #\uFFFD aka � . Thus two byte strings that agree on their UTF-8 characters are equal with the lossy scheme --- nevermind the non-UTF-8 chars.

A potential, easy fix is to use a byte string in step 4 above.

That might not work, though, because we push the data to a Postgres column with the TEXT type. I don't know what TEXT means ... does it also convert bytes to UTF-8? We can try and see.

If TEXT does convert, then we need to change step 4 and change the table schema.

Move the docs to some other more visible place than some markdown files in a branch of the repo. Options include either the built-in repo wiki on the github or scribble, which would integrate nicely with the default racket docs.

1. Is DrRacket fast enough without debugging info? What things need to be disabled?
2. Can Forge disable debugging etc. automatically?

Seems that Forge throws errors when we use parens instead of brackets for function application. Need to either enforce that fun/pred definitions only use brackets or that parens/brackets are interchangeable in this sense. See https://piazza.com/class/k47gct456or1u6?cid=275

I often change theme settings for runs to make the visualizations easier to understand (e.g. making something display as an attribute, changing the color, etc.) It would be great if these settings could be saved when clicking the Next button or even between runs so I don't have to change it every time!

See f2e36c
Assigning to myself.

Swapping to Pardinus moved target-oriented mode into a new option; need to re-integrate optimization (and prevent generating these models unless they're explicitly asked for somewhere?)

sig Thing {}
test expect {
  disjWorks : { some disj x1, x2: Thing | x1 = x2 } is unsat
}

This test fails.

When I try to run forge on the following code I get an error:

#lang forge

sig Node {edges: set Node}

run {}

The error is:

raco test: "temp.rkt"
Forge Version: 0.3.0 - File: /home/ryan/documents/cs_1950y/exercises/forge2/temp.rkt
error writing to stream port
system error: Broken pipe; errno=32
context...:
/home/ryan/.racket/7.5/pkgs/forge/sigs.rkt:489:2: for-loop
/home/ryan/.racket/7.5/pkgs/forge/sigs.rkt:398:0: run-spec
"/home/ryan/documents/cs_1950y/exercises/forge2/temp.rkt": [running body]
temp37_0
for-loop
run-module-instance!125
/usr/share/racket/pkgs/compiler-lib/compiler/commands/test.rkt:179:16
temp.rkt: raco test: test raised an exception
1 test passed

A browser window doesn't pop up. This error doesn't occur if I don't include "run {}", so I am guessing this is related to sterling.

I am not sure if this is caused by updating forge or some other change in my system. I don't know how to install/run a specific version of forge, but if someone tells me how, I will try to bisect.

(I also posted this on piazza)

Paste in and run:

#lang forge/core
(define Node (rel '(univ) 'univ "Node"))
(set ([x Node]) (in x (-> Node Node)))

The arity mismatch in the third line produces an error but with no highlighting. The syntax loc captured is:
#(struct:srcloc forge-core-mod #f #f #f #f). In contrast, the same expression entered in the interactions window produces proper error highlighting. Likewise, a similar error in forge (Alloy syntax) produces highlighthing.

Is this really specific to definitions in forge/core only?

At the moment, we use raw names for wheats and chaffs when downloading them, making it easy to see how to catch the chaffs for students.

Check-ex-spec downloads compiled versions of the wheats and chaffs so that students are unable to read the solution code. However, if a forge/core file imports a wheat (in #lang forge/core), it can print the predicate, thus exposing the solution code. There needs to be some way of hiding the contents of a predicate from this kind of interaction (ideally so that we can make it only usable via check-ex-spec).

Example exploit:

1. Create and run file with contents:

#lang forge/check-ex-spec "forge2/undirected_tree"

2. In same directory, create and run file with contents:

#lang forge/core

(require "wheat_undirected_tree.rkt")

isUndirectedTree

Depends on #58.

Since we are going to be using Electrum for state in 2021, reference to the old traces syntax need to be replaced -- docs, templates, test suite, etc.

Also, need to decide how concrete instances will interact with Electrum. Can I exact-bound variable sigs and relations? (It's possible this will just work out of the box, but we need to check.)

I had to reinstall forge and it now doesn't open Sterling properly, it instead starts up a particular standalone app on my system (which might be built with Electron or similar). I'm running (out of date) Debian sid (unstable), and everything that this page mentions points correctly to Firefox or Chromium. Any ideas?

At the very least, by the lastchecker.rkt and other descents.