Skip to content
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

Induct flag only adds decreases check if type checker is enabled #657

Merged
merged 3 commits into from
Sep 11, 2019

Conversation

Gorzen
Copy link
Contributor

@Gorzen Gorzen commented Aug 29, 2019

No description provided.

Copy link
Member

@romac romac left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please explain the rationale for this change? It seems to me that this commit does not actually change the behaviour of the test suite, is that right?

EDIT: By change I mean the second commit: 936f5f2

@jad-hamza
Copy link
Contributor

Can you please explain the rationale for this change? It seems to me that this commit does not actually change the behaviour of the test suite, is that right?

EDIT: By change I mean the second commit: 936f5f2

The problem is that in the test suite, there are two contexts (one empty, and one with the correct options), and it looks like the empty context was used for the pipeline (and the type-checker option was off during InductElimination).

@romac
Copy link
Member

romac commented Sep 2, 2019

@jad-hamza I see, thanks!

@Gorzen
Copy link
Contributor Author

Gorzen commented Sep 5, 2019

fixes #644

@romac
Copy link
Member

romac commented Sep 5, 2019

@Gorzen Can you please check why the build failed?

@Gorzen
Copy link
Contributor Author

Gorzen commented Sep 5, 2019

@Gorzen Can you please check why the build failed?

It's because of ParialCompiler and BodyEnsuring, check-models fails on them.
However, something weird is that I have the same issues on the master branch.

@romac romac self-requested a review September 5, 2019 11:25
@romac romac added the blocked Blocked by another issue/PR label Sep 5, 2019
@romac
Copy link
Member

romac commented Sep 5, 2019

Blocked by #676

@romac romac removed the blocked Blocked by another issue/PR label Sep 6, 2019
@Gorzen
Copy link
Contributor Author

Gorzen commented Sep 11, 2019

This may break caching in ComponentTestSuite, but as of right now options aren't passed properly to the extractor. (TypeCheckerEnabled) Which causes the tests to break as now we only add decreases if the type checker is enabled.

@romac
Copy link
Member

romac commented Sep 11, 2019

Nice, thanks!

@romac romac merged commit df9f358 into epfl-lara:master Sep 11, 2019
@Gorzen Gorzen mentioned this pull request Oct 3, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants