search

JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

First batch of merges #13

Closed sjjs7 closed 4 years ago

sjjs7 commented 4 years ago

The first 33 commits merged with no conflict. Along with those commits, the 6 that were previously skipped also got merged in. Also ignore commits ab02208 and d458a41, I was experimenting- sorry about that, hopefully you can choose not to merge those.

sjjs7 commented 4 years ago

I also didn't fix the merge conflict the first time in 30c70f3 but corrected myself in the following commits. Hopefully now I can fix conflict in just 1 commit!

I also changed holtest and the Makefile in Mizar because they were causing bugs.

JacquesCarette commented 4 years ago

I'll wait until you give me the final green light to merge, but as far as I can tell, this looks good.

JacquesCarette commented 4 years ago

I approved the extra change, not necessarily the whole thing. holtest is still broken, right?

sjjs7 commented 4 years ago

Yes correct. As soon as I get Ocaml up and running on this other server I will run plain hol light's holtest to use as a comparison against running plain hol QE's holtest.

I understand I'm comparing the time it takes to run files they have in common? I believe time is already being measured in the holtest file so all I need to do is run and save output.

On Sat., Jun. 6, 2020, 10:24 a.m. Jacques Carette, notifications@github.com wrote:

I approved the extra change, not necessarily the whole thing. holtest is still broken, right?

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/JacquesCarette/hol-light-qe/pull/13#issuecomment-640069028, or unsubscribe https://github.com/notifications/unsubscribe-auth/APPK65ERD6XDLTONN43PPZTRVJGS7ANCNFSM4NRW5E3Q .

sjjs7 commented 4 years ago

That one merge was me trying to merge to a branch other than master. I got it now!

JacquesCarette commented 4 years ago

Yes, you want to compare the ones that are in common. Good that it already measures time.

Hopefully, the increased access that Derek gave you will help. I'm surprised it's this hard! Normally, opam, especially on linuxes, is easy to install.

sjjs7 commented 4 years ago

Yeah, I'm not sure what I was doing wrong- I couldn't get the bubblewrap to install. So this time I'll try downloading opam the not-from-scratch way.

JacquesCarette commented 4 years ago

It still depends on blwrap, AFAIK, so that will need to be installed somehow. Hopefully the package manager(s) can deal with it gracefully.

sjjs7 commented 4 years ago

I pushed a bunch more merge commits to master by mistake! It wasn't a lot, I'll make sure to be more careful.

sjjs7 commented 4 years ago

Just going to triple check these work fine, I will let you know ASAP.

JacquesCarette commented 4 years ago

Thanks.

sjjs7 commented 4 years ago

Alright, looks good to go.

JacquesCarette commented 4 years ago

Great - done!

JacquesCarette commented 4 years ago

Note that you should, in general, do further merges into a different branch than 'master' on your fork.