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.

Sign up for GitHub

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

Jump to bottom

Remove DrNim #130

Closed
wants to merge 2 commits into from
Closed

Remove DrNim #130

wants to merge 2 commits into from

Conversation

juancarlospaco
Copy link
Contributor

@juancarlospaco juancarlospaco commented Dec 22, 2021 •
edited
Loading

Remove DrNim

  • Remove DrNim

@juancarlospaco juancarlospaco changed the title wip Remove DrNim Dec 22, 2021
@juancarlospaco juancarlospaco marked this pull request as ready for review December 22, 2021 22:33
alaviss
alaviss reviewed Dec 23, 2021
View reviewed changes
Copy link
Contributor

@alaviss alaviss left a comment

Choose a reason for hiding this comment

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

Right now I disagree with removing Dr. Nim, its code could be useful when we want to make nimskull provable.

@juancarlospaco
Copy link
Contributor Author

I disagree with your disagreement.

@saem
Copy link
Collaborator

saem commented Dec 23, 2021

I've looked at drnim code and I see the promise... and the problems.

We do need something to head in the proving direction, so the real question is are we getting rid of dead code or do a few of the tests run and anchor one or two guarantees.

Why even one or two guarantees? Because even something small can anchor the idea and fundamental concepts of the proving direction.

@haxscramper
Copy link
Collaborator

There are also some error message diagnostics that were added with drnim https://github.com/nim-lang/Nim/blob/7a5314c571ec2c370f63d5fab0afd336e04ec161/compiler/sempass2.nim#L759 and other changes to sempass nim-lang/Nim@3a2697d also need to be accounted for.

@juancarlospaco
Copy link
Contributor Author

I've looked at drnim code and I see the promise... and the problems.

But it is empty promises and problems for no real concrete practical reason.

It would be better to just have a proper DbC module in StdLib without hacks in the compiler like D lang has.

@haxscramper
Copy link
Collaborator

For commit message, you can use your explanation from the nim-lang/RFCs#431

It can be added that correctness prover is an important tool, but preferably it should be implemented as an external application that uses stabilized compiler API rather than hacked-in support into the main compiler.

Right now we don't have necessary resources to support development or maintain drnim, so I also think this removal is justified.

@haxscramper haxscramper added the commit style Commit message need to be fixed according to the contribution guideline label Dec 30, 2021
@haxscramper
Copy link
Collaborator

haxscramper commented Dec 30, 2021 •
edited
Loading

While I have no objections to the PR itself, commit messages must conform to the minimal requirements as explained in the contribution guidelines.

In this specific instance, "why" part of the commit message is unclear - as indicated above, this can be solved by simply reusing the explanation from the RFC.

@haxscramper haxscramper mentioned this pull request Jan 12, 2022
Closed
krux02
krux02 reviewed Jan 16, 2022
View reviewed changes
compiler/modulegraphs.nim
initStrTables(g, m)

proc registerModuleById*(g: ModuleGraph; m: FileIndex) =
registerModule(g, g.packed[int m].module)

proc initOperators*(g: ModuleGraph): Operators =
# These are safe for IC.
# Public because it's used by DrNim.
Copy link
Contributor

Choose a reason for hiding this comment

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

when DrNim is removed that means this can become private again?

haxscramper added a commit to haxscramper/nimskull that referenced this pull request Jan 27, 2022
@haxscramper
Unbundle drnim
b492d90 
- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With dod
  refactor this task becomes much easier, since extra metada can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool it would be easier to
  remove it for now and come up with a proper implementation later on, or
  wen can turn all hacks back into sem.
- Not testsed as a part of CI so right now it can't even be built, due to
  file reorganization nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.
@haxscramper haxscramper mentioned this pull request Jan 27, 2022
Merged
haxscramper added a commit to haxscramper/nimskull that referenced this pull request Jan 27, 2022
@haxscramper
Unbundle drnim
3b2fd08 
- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself not tested as a part of CI so right now it can't even be
  built, due to file reorganization
  nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.
haxscramper added a commit to haxscramper/nimskull that referenced this pull request Jan 27, 2022
@haxscramper
Unbundle drnim
523643a 
- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself not tested as a part of CI so right now it can't even be
  built, due to file reorganization
  nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.
haxscramper added a commit to haxscramper/nimskull that referenced this pull request Jan 27, 2022
@haxscramper
Unbundle drnim
f647a5f 
- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself not tested as a part of CI so right now it can't even be
  built, due to file reorganization
  nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.
haxscramper added a commit to haxscramper/nimskull that referenced this pull request Jan 27, 2022
@haxscramper
Unbundle drnim
e79c703 
- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself not tested as a part of CI so right now it can't even be
  built, due to file reorganization
  nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.
bors bot added a commit that referenced this pull request Jan 28, 2022
@bors @haxscramper
Merge #207
afbd5fe 
207: Unbundle drnim r=saem a=haxscramper

- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself Not tested as a part of CI so right now it can't even be built, due to
  file reorganization #177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  #94 for structured reports.

Closes #130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.



Co-authored-by: haxscramper <haxscramper@gmail.com>
@bors bors bot closed this in 848b6b6 Jan 28, 2022
@haxscramper haxscramper added this to the Sem phase refactoring milestone Nov 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@krux02 krux02 krux02 left review comments

@alaviss alaviss alaviss left review comments

Assignees
No one assigned
Labels
commit style Commit message need to be fixed according to the contribution guideline
Projects
None yet
Milestone
Semantic analysis phase refactoring
Development

Successfully merging this pull request may close these issues.
5 participants
@juancarlospaco @saem @haxscramper @krux02 @alaviss