You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hey guys,
I found another issue, you may not know about:
When trying Cosette with a big chunk of queries, I had it freeze on one test:
schema schema_film_actor (last_update:Date, actor_id:Integer, film_id:Integer);
table film_actor(schema_film_actor);
schema schema_film (special_features:String, rental_duration:Integer, rental_rate:Double, release_year:Integer, length:Integer, replacement_cost:Double, rating:String, description:String, language_id:Integer, title:String, original_language_id:Integer, last_update:Date, film_id:Integer);
table film(schema_film);
query student
`SELECT DISTINCT t_0.film_id, t_0.title FROM film t_0, film t_1, film_actor t_2, film_actor t_3, film_actor t_4, film_actor t_5 WHERE NOT t_4.actor_id = t_2.actor_id AND t_4.actor_id = t_5.actor_id AND t_2.actor_id = t_3.actor_id AND t_2.film_id = t_0.film_id AND t_4.film_id = t_0.film_id AND t_3.film_id = t_1.film_id AND t_5.film_id = t_1.film_id AND t_0.rental_rate > (t_1.rental_rate * 2)`;
query master
`SELECT DISTINCT t_0.film_id, t_0.title FROM film t_0, film t_1, film_actor t_2, film_actor t_3, film_actor t_4, film_actor t_5`;
verify student master
I had the process: /HoTT/coq-HoTT/bin/coqtop -coqlib /usr/local/share/hott/coq -R /usr/local/share/hott/theories HoTT -Q /usr/local/share/hott/contrib -indices-matter -q -R . Cosette -compile WCiEiXyyQYrrQ.v
running a couple hours on 100% for one core of my CPU.
After I killed it, Cosette gave me the result:
Also, because it was pretty late already, I yesterday submitted the query to your Cosette Online Demo: https://demo.cosette.cs.washington.edu/ It is not available for me anymore (502 Proxy Error), I think I just broke your website, I'm sorry... :(
You should think about implementing some kind of timeout in your python script to kill threads like this, that do not get catched by the implemented timeout method.
EDIT: The website seems to be back up, which is nice. However, I would suggest you test it out for yourselfs with the query. I'm a little afraid to touch your webinterface again ;-)
The text was updated successfully, but these errors were encountered:
Hey guys,
I found another issue, you may not know about:
When trying Cosette with a big chunk of queries, I had it freeze on one test:
I had the process:
/HoTT/coq-HoTT/bin/coqtop -coqlib /usr/local/share/hott/coq -R /usr/local/share/hott/theories HoTT -Q /usr/local/share/hott/contrib -indices-matter -q -R . Cosette -compile WCiEiXyyQYrrQ.v
running a couple hours on 100% for one core of my CPU.
After I killed it, Cosette gave me the result:
CLICK ME
` {"rosette_log": "Rosette find an counterexample.", "coq_result": "ERROR", "coq_log": "Invalid generated Coq code. Please file an issue.", "rosette_source": "#lang rosette \n \n(require \"../cosette.rkt\" \"../sql.rkt\" \"../evaluator.rkt\" \"../syntax.rkt\") \n \n(provide ros-instance)\n \n(current-bitwidth #f)\n \n(define-symbolic div_ (~> integer? integer? integer?))\n \n(define film-info (table-info \"film\" (list \"special_features\" \"rental_duration\" \"rental_rate\" \"release_year\" \"length\" \"replacement_cost\" \"rating\" \"description\" \"language_id\" \"title\" \"original_language_id\" \"last_update\" \"film_id\")))\n \n(define film_actor-info (table-info \"film_actor\" (list \"last_update\" \"actor_id\" \"film_id\")))\n \n\n(define (student tables) \n (SELECT-DISTINCT (VALS \"t_0.film_id\" \"t_0.title\") \n FROM (JOIN (AS (NAMED (list-ref tables 0)) [\"t_0\"]) (JOIN (AS (NAMED (list-ref tables 0)) [\"t_1\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_2\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_3\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_4\"]) (AS (NAMED (list-ref tables 1)) [\"t_5\"])))))) \n WHERE (AND (AND (AND (AND (AND (AND (AND (NOT (BINOP \"t_4.actor_id\" = \"t_2.actor_id\")) (BINOP \"t_4.actor_id\" = \"t_5.actor_id\")) (BINOP \"t_2.actor_id\" = \"t_3.actor_id\")) (BINOP \"t_2.film_id\" = \"t_0.film_id\")) (BINOP \"t_4.film_id\" = \"t_0.film_id\")) (BINOP \"t_3.film_id\" = \"t_1.film_id\")) (BINOP \"t_5.film_id\" = \"t_1.film_id\")) (BINOP \"t_0.rental_rate\" > (VAL-BINOP \"t_1.rental_rate\" * 2)))))\n\n(define (master tables) \n (SELECT-DISTINCT (VALS \"t_0.film_id\" \"t_0.title\") \n FROM (JOIN (AS (NAMED (list-ref tables 0)) [\"t_0\"]) (JOIN (AS (NAMED (list-ref tables 0)) [\"t_1\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_2\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_3\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_4\"]) (AS (NAMED (list-ref tables 1)) [\"t_5\"])))))) \n WHERE (TRUE)))\n\n\n(define ros-instance (list student master (list film-info film_actor-info))) \n", "result": "ERROR", "counterexamples": [{"table-content": [["special_features", "rental_duration", "rental_rate", "release_year", "length", "replacement_cost", "rating", "description", "language_id", "title", "original_language_id", "last_update", "film_id"], [[[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 15]]], "table-name": "film"}, {"table-content": [["last_update", "actor_id", "film_id"], [[[0, 0, 0], 2]]], "table-name": "film_actor"}], "rosette_result": "NEQ", "error_msg": "Invalid generated Coq code. Please file an issue. \n \n Rosette find an counterexample.", "coq_source": "Require Import HoTT. \nRequire Import UnivalenceAxiom. \nRequire Import HoTTEx. \nRequire Import Denotation. \nRequire Import UnivalentSemantics. \nRequire Import AutoTactics. \nRequire Import CQTactics. \n \nOpen Scope type. \n \nModule Optimization (T : Types) (S : Schemas T) (R : Relations T S) (A : Aggregators T S). \n Import T S R A. \n Module SQL_TSRA := SQL T S R A. \n Import SQL_TSRA. \n Module AutoTac := AutoTactics T S R A. \n Import AutoTac. \n Module CQTac := CQTactics T S R A. \n Import CQTac. \n \n Notation combine' := combineGroupByProj.\n \n Parameter count : forall {T}, aggregator T int. \n Notation \"'COUNT' ( e )\" := (aggregatorGroupByProj count e). \n Parameter sum : forall {T}, aggregator T int. \n Notation \"'SUM' ( e )\" := (aggregatorGroupByProj sum e). \n Parameter max : forall {T}, aggregator T int. \n Notation \"'MAX' ( e )\" := (aggregatorGroupByProj max e). \n Parameter min : forall {T}, aggregator T int. \n Notation \"'MIN' ( e )\" := (aggregatorGroupByProj min e). \n Parameter avg : forall {T}, aggregator T int. \n Notation \"'AVG' ( e )\" := (aggregatorGroupByProj avg e).\n \n Parameter gt: Pred (node (leaf int) (leaf int)). \n \n Variable integer_2: constant int. \n\n\n Definition Rule: Type. \n refine (forall ( \u0393 scm_schema_film scm_schema_film_actor: Schema) (rel_film: relation scm_schema_film) (rel_film_actor: relation scm_schema_film_actor) (schema_film_special_features : Column int scm_schema_film) (schema_film_rental_duration : Column int scm_schema_film) (schema_film_rental_rate : Column int scm_schema_film) (schema_film_release_year : Column int scm_schema_film) (schema_film_length : Column int scm_schema_film) (schema_film_replacement_cost : Column int scm_schema_film) (schema_film_rating : Column int scm_schema_film) (schema_film_description : Column int scm_schema_film) (schema_film_language_id : Column int scm_schema_film) (schema_film_title : Column int scm_schema_film) (schema_film_original_language_id : Column int scm_schema_film) (schema_film_last_update : Column int scm_schema_film) (schema_film_film_id : Column int scm_schema_film) (schema_film_actor_last_update : Column int scm_schema_film_actor) (schema_film_actor_actor_id : Column int scm_schema_film_actor) (schema_film_actor_film_id : Column int scm_schema_film_actor), _). \n refine (\u27e6 \u0393 \u22a2 DISTINCT (SELECT1 (combine (right\u22c5left\u22c5schema_film_film_id) (right\u22c5left\u22c5schema_film_title)) FROM1 (product (table rel_film) (product (table rel_film) (product (table rel_film_actor) (product (table rel_film_actor) (product (table rel_film_actor) (table rel_film_actor)))))) WHERE (and (and (and (and (and (and (and (negate (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5schema_film_actor_film_id)) (variable (right\u22c5right\u22c5left\u22c5schema_film_film_id)))) (castPred (combine (right\u22c5left\u22c5schema_film_rental_rate) (e2p (binaryExpr times_ (variable (right\u22c5right\u22c5left\u22c5schema_film_rental_rate)) (constantExpr integer_2))) ) gt))) : _ \u27e7 = \u27e6 \u0393 \u22a2 DISTINCT (SELECT1 (combine (right\u22c5left\u22c5schema_film_film_id) (right\u22c5left\u22c5schema_film_title)) FROM1 (product (table rel_film) (product (table rel_film) (product (table rel_film_actor) (product (table rel_film_actor) (product (table rel_film_actor) (table rel_film_actor)))))) ) : _ \u27e7). \n Defined. \n Arguments Rule /. \n \n Lemma ruleStand: Rule. \n start;\n first [sum_heuristic1| prod_heuristic1| deductive_proof'| conjunctiveQueryProof'| hott_ring']. \n Qed. \n \nEnd Optimization. \n"} `
Also, because it was pretty late already, I yesterday submitted the query to your Cosette Online Demo:
https://demo.cosette.cs.washington.edu/
It is not available for me anymore (502 Proxy Error), I think I just broke your website, I'm sorry... :(
You should think about implementing some kind of timeout in your python script to kill threads like this, that do not get catched by the implemented timeout method.
EDIT: The website seems to be back up, which is nice. However, I would suggest you test it out for yourselfs with the query. I'm a little afraid to touch your webinterface again ;-)
The text was updated successfully, but these errors were encountered: