New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some improvements and unifier fixes #1558

Merged
merged 12 commits into from Oct 12, 2018

Conversation

Projects
None yet
2 participants
@mtzguido
Contributor

mtzguido commented Oct 8, 2018

Making this branch so @nikswamy can review some of the changes, as they touch core components.

This branch fixes #1443, #1523 and part of #1514 (@aseemr has the other piece for that).

The most sensitive changes, IMO, are the tc: ones.

@mtzguido mtzguido requested a review from nikswamy Oct 8, 2018

let wl = {wl' with attempting=rest} in
let wl = {wl with wl_implicits = wl'.wl_implicits @ imps} in

This comment has been minimized.

@nikswamy

nikswamy Oct 8, 2018

Contributor

This looks good.

Although, FYI, the general structure here is similar to what is provided by try_solve_without_smt_or_else (also in this module). I wonder if we should refactor a bit.

@nikswamy

nikswamy Oct 8, 2018

Contributor

This looks good.

Although, FYI, the general structure here is similar to what is provided by try_solve_without_smt_or_else (also in this module). I wonder if we should refactor a bit.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 8, 2018

Contributor

Ouch, still slightly broken.. typechecking examples/native_tactics/Simple.fst makes #1091 pop up, but only without two phases. I can follow tomorrow, sorry for the noise.

Contributor

mtzguido commented Oct 8, 2018

Ouch, still slightly broken.. typechecking examples/native_tactics/Simple.fst makes #1091 pop up, but only without two phases. I can follow tomorrow, sorry for the noise.

mtzguido added some commits Oct 8, 2018

tc: term: track some implicit in annotations being lost
We were checking the types for each let rec, but not tracking the
implicits that they might have. This is needed, as the many repros in
 #1443 show.
tc: rel: tracking implicits that were being lost
Calling solve_t might return new implicits, which we must again keep
track of. To make sure we don't duplicate the implicits we're tracking,
we do the call with an empty list of implicits, and then we append the
result to the implicits we were already carrying.

c.f. #1443 and #1523
@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 9, 2018

Contributor

I think the new failure is more of an instance of #933 than of #1091, i.e. a bad decreases clause, uncovered by the fix to the unifier. I worked around it for now, as it seems caused by a different issue and only happens without two phases, so I don't think it's a big roadblock.

I would merge this, but we could wait until we fix #933/#1091 if you want, Nik.

Contributor

mtzguido commented Oct 9, 2018

I think the new failure is more of an instance of #933 than of #1091, i.e. a bad decreases clause, uncovered by the fix to the unifier. I worked around it for now, as it seems caused by a different issue and only happens without two phases, so I don't think it's a big roadblock.

I would merge this, but we could wait until we fix #933/#1091 if you want, Nik.

mtzguido added some commits Oct 10, 2018

@nikswamy

Thanks Guido. This looks good overall.
The increased severity of #933 seems slight. I'd go for merging this, provided we also pass regressions on everest-ci.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 11, 2018

Contributor

I did get a failure in everest when I kicked a CI build, trying to repro locally now. I'll report back here.

Contributor

mtzguido commented Oct 11, 2018

I did get a failure in everest when I kicked a CI build, trying to repro locally now. I'll report back here.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 12, 2018

Contributor

Fixed the HACL* failure in project-everest/hacl-star@431157d, and got an everest green with that, so I think we're good to go.

Contributor

mtzguido commented Oct 12, 2018

Fixed the HACL* failure in project-everest/hacl-star@431157d, and got an everest green with that, so I think we're good to go.

@mtzguido mtzguido merged commit b4a02d0 into master Oct 12, 2018

1 check passed

FStar-Linux #FStar-Linux-20181012-6 succeeded
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment