David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement tags.
I'm away from my main computer... can you add them ?
Actually, most *OLD and *ALT should probably have both discouragement tags
as well, it seems ?
Thanks,
Benoît
On Thursday, February 13, 2020 at 9:13:39 AM UTC+1,
I realize that it seems especially inconvenient that moving df-gsum back
requires moving df-0g back too. But this better reflects the reality,
because df-gsum not allowed to refer to constants defined after cgsum
anyway (to prevent cycles), and placing df-gsum much further along just
makes this
On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote:
>
> David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement
> tags. I'm away from my main computer... can you add them ?
>
> Actually, most *OLD and *ALT should probably have both discouragement tags
> as well, it
On Thursday, February 13, 2020 at 5:06:27 PM UTC+1, Norman Megill wrote:
>
> On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote:
>>
>> David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement
>> tags. I'm away from my main computer... can you add them ?
>>
>> Actually,
"David A. Wheeler" wrote:
> I've just posted an updated "jobs" system if you want to do
> big-scale minimization, especially if you're using a number of cores.
>
> This version supports disjoint sets of jobs, e.g., you can now say:
> scripts/jobs 112 125-132 144-151
> That means the API has
I'm trying out 123 and 124 for now using AWS. I might be able to scale up
depending on the results.
On Thu, Feb 13, 2020 at 4:51 PM David Starner wrote:
> On Thu, Feb 13, 2020 at 2:28 PM Norman Megill wrote:
> >
> > Here is an update of current commitments as of Feb. 13, 17:30 EST :
> >
> >
Most of the definitions don't need to be moved up, only the "structural"
ones that are required for actually defining the content of the new slot.
df-gsum is unfortunate because it is a relatively complex definition that
is also a dependency for the slot, but if you can write the slot without
any
Here is an update of current commitments as of Feb. 13, 17:30 EST :
101 Alexander
102 heiphohmia
103-111 David Starner
112 David A. Wheeler
113-124 UNASSIGNED
125-132 David A. Wheeler
133-134 UNASSIGNED
135-143 David Starner
144-151 David A. Wheeler
152-160 UNASSIGNED
Thierry has volunteered
I've just posted an updated "jobs" system if you want to do
big-scale minimization, especially if you're using a number of cores.
This version supports disjoint sets of jobs, e.g., you can now say:
scripts/jobs 112 125-132 144-151
That means the API has changed, but I think it's for the better.
On Thu, Feb 13, 2020 at 2:28 PM Norman Megill wrote:
>
> Here is an update of current commitments as of Feb. 13, 17:30 EST :
>
> 101 Alexander
> 102 heiphohmia
> 103-111 David Starner
> 112 David A. Wheeler
> 113-124 UNASSIGNED
> 125-132 David A. Wheeler
> 133-134 UNASSIGNED
> 135-143 David
I worked out an estimate (in hours) for jobs 133-160 based on the theory
that the time to save a compressed proof is proportional to the run time of
'minimize'. Here's how it compares so far, assuming a CPU taking about 30
sec for the 3atlem4 minimization. I'll keep this updated as the logs
On Thu, Feb 13, 2020 at 6:47 PM David A. Wheeler wrote:
> David S.: what kind of computer are you using? Some laptop temperature
> sensors do not work properly, and in general laptops are not designed to
> sustain computation at maximum for a long time. It is possible that the
> segfaults are
Okay, I will hold off on 123 and 124.
Mario Carneiro wrote:
> I'm trying out 123 and 124 for now using AWS. I might be able to scale up
> depending on the results.
>
> On Thu, Feb 13, 2020 at 4:51 PM David Starner wrote:
>
> > On Thu, Feb 13, 2020 at 2:28 PM Norman Megill wrote:
> > >
> > >
On Thursday, February 13, 2020 at 7:51:53 PM UTC-5, David Starner wrote:
>
>
> I had a couple
> unexplained segmentation faults, on job105 and job135. I restarted
> job105 and it ran to completion; I haven't tried restarting 135 yet.
> I'll restart 135 and actually start 137, and take 133, 134,
On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote:
>
> That said, I think it would still be better to move all definitions needed
> for df-prds before it. This is a downside of the "everything structure"
> approach, but it does not displace too many definitions. We can
Hi,
Il 13/02/20 01:13, Norman Megill ha scritto:
> Per request of Giovanni (see
> https://groups.google.com/d/msg/metamath/uSa8Q0fWKeM/9dDcUM-DCwAJ ) I
> also did the following. I assume this is still desired?
>
> git commit -m'Release version 0.181.'
> git tag v0.181
> git
16 matches
Mail list logo
