tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

check-ex-spec logging #67

Closed bennn closed 3 years ago

bennn commented 3 years ago

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

Example research questions:

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

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

bennn commented 3 years ago

I made a SQL instance:

Google Cloud MySQL instance
- ID : cs1710-2021-examplar
- password : drracket
- connection name : pyret-examples:us-east1:cs1710-2021-examplar
- public IP : 34.75.228.82

and a database cs1710_2021_examplar and a table checkexspec

CREATE TABLE checkexspec (
 id serial PRIMARY KEY,
 ts TIMESTAMP DEFAULT CURRENT_TIMESTAMP,
 ip CHAR(4),
 local_id INT UNSIGNED,
 student VARCHAR(30),
 project VARCHAR(30),
 input MEDIUMTEXT,
 output MEDIUMTEXT
);

and also a cloud function, but I still need to test that.

EDIT 2021-01-25 Dear diary ... I have a cloud function that properly updates the SQL database when run from the Google Cloud "Testing" tab, but when I send a JSON from my own machine the database always gets an empty row. Back to work.

bennn commented 3 years ago

The cloud function seems to work. Here's a racket script that I was able to run locally to put something in the database:

#lang racket/base

(require
  json
  net/uri-codec
  net/url)

(define trigger-url
  (string->url
    "https://us-east1-pyret-examples.cloudfunctions.net/cs1710-2021-examplar"))

(define (test js)
  (define str (jsexpr->string js))
  (define-values [status head* inp]
    (http-sendrecv/url
      trigger-url
      #:method "POST"
      #:data str
      #:headers (list "Content-Type: application/json; charset=UTF-8")))
  (void
    (for ((ln (in-lines inp)))
      (printf "  ~s~n" ln)))
  (close-input-port inp)
  (void))

;;(test #hash())
;; adds empty row

(test #hash((local_id . 42)
            (student . "test_student")
            (project . "test_project")
            (input . "test_in")
            (output . "test_out")))
;; adds NON-empty row
bennn commented 3 years ago

84 brings these in, but the standard forge logging should have everything anyway