Re: [Metamath] Question abouot indistopon

e: > Thank you for the pointer, Mario. Is this negative vs. positive position > terminology something you neologized on the fly? Or does it have > precedent? If > I'm grokking you correctly, the positive positions plug into the negative > positions, which jibes with your explanation an

Re: [Metamath] Mnemonic of Fr

My understanding is that it stands for "founded relation", as in well-founded but without the "well", I think because it doesn't have any other ordering properties like being a partial order attached to it. On Wed, May 1, 2024 at 5:21 AM 'B. Wilson' via Metamath < metamath@googlegroups.com>

Re: [Metamath] Question abouot indistopon

There is a convention, which is to use "( A e. V -> ..." in antecedents to theorems and deduction-form statements and |- A e. _V in inference-form theorems. In "positive position", you often need to use A e. _V, i.e. in fvex there is no other reasonable option for what set to say that function

Re: [Metamath] Trying to understand 2p2e4

. >> Internally, it only creates and manipulates the numbers, it doesn't >> actually perform the expansion (which would take exponentially long just to >> output). For the former number (12178 steps), an approximation to this is >> to just "show proof *" which will pri

Re: [Metamath] Trying to understand 2p2e4

10^12 steps if you are interested in such a programming project. But be aware that the steps can also get pretty large in the process (I think also exponential in general). Although I'm sure your terabyte drive has better things to do... Mario Carneiro On Mon, Apr 1, 2024 at 9:44 AM Anarcocap

Re: [Metamath] Re: Meaning of "JFM"

Yes, these are references to the Mizar Mathematical Library, as published in the Journal of Formalized Mathematics. On Sat, Mar 30, 2024 at 4:58 PM Glauco wrote: > Using Gemini and some luck, could it be Journal Of Formalized Mathematics > ? > > -- > You received this message because you are

Re: [Metamath] Help building hmm (Haskell Metamath verifier)

Regarding the Haskell errors, do you have warnings-as-errors on? It seems like all of the errors are actually just promoted warnings, so possibly you can just disable those warnings. On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett wrote: > I've been trying to add hmm to metamath-docker, because

Re: [Metamath] Help building hmm (Haskell Metamath verifier)

On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett wrote: > The more I think about it, the more any attempt to maintain metamath-test > without containerization seems insane. You need to have C, C++, Rust, > Java, Python, and Haskell installed, then use them to build metamath.exe, > checkmm,

Re: [Metamath] metamath-test added to metamath-cmds docker image

kmmc set.mm > Time (mean ± σ): 34.860 s ± 0.949 s[User: 30.446 s, System: > 4.412 s] > Range (min … max): 34.097 s … 37.491 s10 runs > > Warning: Statistical outliers were detected. Consider re-running this > benchmark on a quiet system without any interference

Re: [Metamath] metamath-test added to metamath-cmds docker image

As far as I know and last I checked, metamath-knife can check set.mm in sub-one-second with verification enabled, and about half a second with verification disabled. It's possible that things have changed due to the growth of set.mm? Just checked again: $ cargo build --release $ hyperfine -w 2

Re: [Metamath] Results about ax-13 usage

On Mon, Mar 11, 2024 at 11:36 AM Jim Kingdon wrote: > If this is just a hypothetical question I guess we don't really need to > come up with a definitive answer, but I will say that if we want to keep > some of our other values (like preferring short proofs), we'd end up > with a lot of ALT

Re: [Metamath] Results about ax-13 usage

gh to state what is >> probably obvious but maybe needs to be said anyway, iset.mm does not >> only remove axioms relative to set.mm, it also adds axioms and modifies >> axioms. >> On 1/9/24 19:19, Mario Carneiro wrote: >> >> And of course the largest such refacto

Re: [Metamath] Re: Proof generation

I think mmj2 only ever uses wceq, because it "parses" formulas and using weq introduces an ambiguity into the resulting grammar. However metamath-exe's MINIMIZE will find shorter proofs using lemmas, and it treats syntax lemmas just like real lemmas, so it will "optimize" the proof to use weq. I

Re: [Metamath] Re: Proof generation

On Mon, Feb 12, 2024 at 8:40 AM Glauco wrote: > The proofs produced by mmj2 are not exactly the same, because (in my > opinion) mmj2 has a small bug in the knapsack algorithm > > IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've > shown several examples, in the past) >

Re: [Metamath] Proof generation

The specification for metamath checking in general is given in the Metamath Book: https://us.metamath.org/downloads/metamath.pdf The proof blocks are written in "compressed proof format", which is specified in Appendix B of the metamath book. (Although, metamath-exe, mmj2 and metamath-knife

[Metamath] Re: mm-web-rs server support

free to run https://github.com/digama0/mm-web-rs locally before the beta version goes live. On Thu, Feb 8, 2024 at 1:59 AM Mario Carneiro wrote: > mm-web-rs now supports generation of the auxiliary pages: > mmtheorems.html, mmrecent.html, mmtheoremsall.html, mmdefinition

[Metamath] Re: mm-web-rs server support

build (under an experimental subfolder) so that regular users can play with it and find differences with the original. On Sun, Jan 30, 2022 at 2:43 AM Mario Carneiro wrote: > Hi All, > > I just wanted to share some metamath-knife progress: The > https://github.com/digama0/mm-web-rs

Re: [Metamath] Constant symbols are not allowed in a "$d" statement.

You can't use $d to ensure that constants don't appear in a formula. I don't have all the context needed to understand why you need to do this, but one way to express it would be to have a predicate "|- ^.-free A" and have rules like "|- ( ^.-free A -> ( ^.-free B -> ^.-free ( A /\ B ) ) )" for

Re: [Metamath] mmj2: Unification failure in derivation proof step

The issue is that the '. syntax is ambiguous, A = B '. can be interpreted as either "A = (B '.)" or "(A = B) '." . Syntax ambiguity in set.mm (and most metamath databases) is a big no-no, you can generally prove a contradiction from them, but because mmj2 parses formulas into trees ambiguous

Re: [Metamath] mmj2: Unification failure in derivation proof step

That error message means that the theorem df-bl.tick has a statement that does not match the expression |- ( A = B '. <-> ( A = B ^. 1 ) ) that you have provided. It's difficult to say more without seeing the rest of the code (and in particular, the definition of `df-bl.tick`). Q1: No, this is a

Re: [Metamath] Prime Number Theorem

y to have such a > tool, too. I've been thinking about it for a while. > > BR, > _ > Thierry > > > On 31/01/2024 07:04, Jim Kingdon wrote: > > Looks like Terrence Tao is planning [1] to follow in the footsteps of > Mario Carneiro [2] and formalize the Prime Number Theorem

Re: [Metamath] Results about ax-13 usage

And of course the largest such refactor in this vein is iset.mm, although this one was considered sufficiently different as to be moved to a separate database (which I think is slightly unfortunate). On Tue, Jan 9, 2024 at 10:17 PM Mario Carneiro wrote: > IMO this is definitely worthwh

Re: [Metamath] Results about ax-13 usage

IMO this is definitely worthwhile, especially since it moves an axiom from used almost everywhere to used almost nowhere. We have previously done refactors of that kind for ax-groth, ax-ac2, ax-reg, ax-rep and I think we have a better understanding of the true dependencies of many theorems as a

Re: [Metamath] Results about ax-13 usage

On Mon, Jan 1, 2024 at 6:43 PM Jim Kingdon wrote: > One (historical?) note: some of what we have now is the result of > experimentation in the opposite direction - trying to figure out whether a > logical system can be built without distinct variable constraints at all (I > think there is some

Re: [Metamath] German translation of the Metamath book

Sounds good to me. You should send a PR to https://github.com/metamath/metamath-website-seed, which contains the source for index.html. What are you planning to do with the translated sources? Are they in a separate repo? The site build does run latex for some things although I don't think it

Re: [Metamath] mm0 semantic equivalence

MM0 does not itself do any normalization of expressions. Instead, it acts as a verification tool for already completed proofs, although it has some facilities for constructing proofs and it is extensible enough to let you add more automation to it, which you could use to automate normalization

Re: [Metamath] Website is down

Fixed in https://github.com/metamath/metamath-website-seed/pull/20. On Sun, Nov 12, 2023 at 4:18 AM Mario Carneiro wrote: > Looks like this is because the source was line-broken there, it says > > > > in the source and this is enough to fool the simple image usage heuristic >

Re: [Metamath] Website is down

Looks like this is because the source was line-broken there, it says in the source and this is enough to fool the simple image usage heuristic here: https://github.com/metamath/metamath-website-scripts/blob/8d81a0c1ab3e433b335b4e6a3bdc364d277b4946/build-website.sh#L133 I'm not sure what the

Re: [Metamath] Update: website generation rewrite

m/issues/1887 and > https://github.com/metamath/set.mm/pull/3515. > > Benoît > > > > On Sat, Sep 30, 2023 at 5:08 PM Mario Carneiro wrote: > > There is very little code involved in keeping a file somewhere else, there > is just one cp line in the script. So I'

Re: [Metamath] Website is down

On Wed, Oct 25, 2023 at 3:46 PM Gino Giotto wrote: > From https://us.metamath.org/copyright.html#pd the GNU General Public > License link gives a 404. The top level LICENSE.TXT has been removed, as the web site is PD not GPLv2 (except for some enumerated

Re: [Metamath] Website is down

On Wed, Oct 25, 2023 at 3:46 PM Gino Giotto wrote: > From https://us.metamath.org/ the mmsolitaire.tar.gz > , mpeuni.tar.gz > , qleuni.tar.gz >

Re: [Metamath] Website is down

We have one more test to go, tonight I will let it run on its own. Hopefully all the hotfixes for issues reported here will also be reflected in the updated script. There is also a bit of remaining cleanup to do re: images in set.mm repo. All the _frege_*.svg files are duplicated in seed/mpegif/,

Re: [Metamath] Website is down

I'm afraid tirix will have to fix that himself, I don't know where the source or hosting for that site is. (Although, I think it would be quite possible to integrate those pages into the main site now.) On Wed, Oct 25, 2023 at 1:30 PM Gino Giotto wrote: > From

Re: [Metamath] Website is down

On Wed, Oct 25, 2023 at 1:14 PM Gino Giotto wrote: > Also, I don't know if it's just me, but if I click Recent proofs > which is in the first > box titled > *Metamath Proof Explorer* > from

Re: [Metamath] Website is down

https://us.metamath.org/mpegif/mmset.html include the [Bauer] reference >>> (another litmus test for up to dateness). >>> >>> * https://us.metamath.org/ileuni/mmrecent.html is up to date (shows a >>> revision from 22-Oct-2023) >>> >>> So looks go

Re: [Metamath] Website is down

://us.metamath.org/ileuni/mmrecent.html is up to date (shows a >>> revision from 22-Oct-2023) >>> >>> So looks good! >>> >>> Thanks for all the hard work on this. >>> On 10/25/23 00:33, Mario Carneiro wrote: >>> >>> Sorry

Re: [Metamath] Website is down

Crap, I deleted the site again. Sorry folks, it will be back in 3 hours. On Wed, Oct 25, 2023 at 4:54 AM Mario Carneiro wrote: > Oh, this is probably because the site build was done using the set.mm > branch from https://github.com/metamath/set.mm/pull/3524. I'll have to > rerun the wh

Re: [Metamath] Website is down

Ok, even though "most recent" shows theorems > from 24-Sep-2023. > > The link on the home page https://us.metamath.org/ still points to > http://us2.metamath.org:88/mpeuni/mmrecent.html but that's a different > issue. > > > On 25/10/2023 10:10, Mario Carneiro wrot

Re: [Metamath] Website is down

should be fixed now On Wed, Oct 25, 2023 at 3:39 AM Thierry Arnoux wrote: > https://us.metamath.org/mpeuni/mmrecent.html > > Still throws a 404. > On 25/10/2023 09:33, Mario Carneiro wrote: > > Sorry about that, I chose the wrong time to test the new website build > pro

Re: [Metamath] Website is down

Sorry about that, I chose the wrong time to test the new website build process and the cron job started running in the middle of it, and unfortunately killing the cron job just made it copy an empty website to the live site. Things should be back up now. On that note, what is now up is the new

Re: [Metamath] Order of variables in DV statements

IMO class/wff variables should come at the beginning, with the list of setvars being read as a (non)dependency specification for the class/wff variable. I most recently visited this question for mm-web-rs, which does not put the class/wff variables first - it just sorts all the variables, meaning

Re: [Metamath] Question on definition of magma

On Thu, Oct 12, 2023 at 1:46 AM bil...@gmail.com wrote: > I am at a more basic level than what you are trying to address. My goal is > to learn how to prove theorems in metamath. > > My current task is to do the follow: given B = { x | ph }, how would I > prove that A e. B. This is beginning

Re: [Metamath] Question on definition of magma

Usually we prioritize minimizing the length of the definition (number of symbols) over the length of the extraction theorem, because the former is an axiom and the latter is not. On Thu, Oct 12, 2023 at 12:46 AM bil...@gmail.com wrote: > You say that the definitions are the same, but to me

Re: [Metamath] Question on definition of magma

Those two definitions are the same except you have removed the substitutions b := ( Base ` g ) and o := ( +g ` g ) . The substitutions are there to make the definition more readable (and usually shorter, although it might be a wash in a short definition like this one). For a more elaborate example

Re: [Metamath] Update: website generation rewrite

more supportive of just moving all the database-specific files into set.mm repo if that's what we want to do. On Sat, Sep 30, 2023 at 5:08 PM Mario Carneiro wrote: > There is very little code involved in keeping a file somewhere else, there > is just one cp line in the script. So I'm fine if w

Re: [Metamath] Update: website generation rewrite

mmbiblio.raw.html is hosted on set.mm repo but IL's mmbiblio.raw.html is in the seed repo. Some kind of general rule for where to look for files would be appreciated, the simpler the better. On Sat, Sep 30, 2023 at 1:04 PM Jim Kingdon wrote: > On 9/30/23 04:27, Mario Carneiro wrote: > > Moreo

Re: [Metamath] Update: website generation rewrite

k involved in an .html file versus the .mm file - they can generally be updated in any order, with the main issue being possible broken links if the mm file links to the html file or vice versa before the other has landed. On Sat, Sep 30, 2023 at 7:18 AM Mario Carneiro wrote: > I don't think we

Re: [Metamath] Update: website generation rewrite

ile >> and reloads) and you will get instant feedback (loading individual pages >> takes milliseconds). I've also been contemplating just running this on the >> server directly, so that we don't need to spend gigabytes of space on all >> the precomputed HTML files if it is

Re: [Metamath] Update: website generation rewrite

On 9/29/23 21:52, Mario Carneiro wrote: > > > in my test these are 4893.94 s and 5020.87 s respectively (that is, > > 2h45m total). I just got the new version working, and it takes 10.8 s > > and 11.1 s respectively > > Exciting stuff! > > This has me ponde

[Metamath] Update: website generation rewrite

For those who aren't aware, I've been working on a rewrite of the website generation code. The main PR is https://github.com/metamath/metamath-website-scripts/pull/16 , with links to other parts of the process. I wanted to share another milestone: I'm also writing

Re: [Metamath] Question on Theorem pm2.61ne

No, set.mm is working in ZFC, or rather a conservative extension thereof. Classes are ZFC classes, they cannot be quantified but they represent maybe-proper classes in the usual way. They are not "in the universe" in the sense that "A. x ph" ranges over all sets, and proper classes are not

Re: [Metamath] Question on Theorem pm2.61ne

(copying my answer, something odd seems to have happened to the first post) The first assumption ( A = B -> ( ps <-> ch ) ) is the idiomatic way to say that ch is the result of substituting A for B in ps, and there are many theorems that produce results of this form. The theorem is still true

Re: [Metamath] Question on Theorem pm2.61ne

The first assumption ( A = B -> ( ps <-> ch ) ) is the idiomatic way to say that ch is the result of substituting A for B in ps, and there are many theorems that produce results of this form. The theorem is still true when you only have a one-directional implication (in fact the first step of the

Re: [Metamath] ?Statement "a3" cannot be unified with step 25.

axiom a3 is missing parentheses around it On Sun, Aug 13, 2023 at 5:30 PM Jeroen van Rensen wrote: > Hello everyone, > > I am trying to prove the following statement: > > ! ! p |- p > > The formal proof is as follows (the axioms are the same as in set.mm): > > 1. ! ! p (Premiss) > 2. ! ! p ->

Re: [Metamath] Substitute wff for a variable

Actually you have the same syntax error in a1 and a2, the outermost implication should be surrounded in parentheses. Since you declared the implication symbol with parentheses around it they are required for any implication and cannot be omitted. On Fri, Aug 11, 2023 at 11:47 AM Mario Carneiro

Re: [Metamath] Substitute wff for a variable

you have a syntax error in `maj` , it should read |- ( p -> q ) instead of |- p -> q. With the incorrect statement it won't be able to unify when you try to apply it. On Fri, Aug 11, 2023 at 11:45 AM Jeroen van Rensen < jeroenvanren...@gmail.com> wrote: > Hello everyone, > > I'm new to Metamath

Re: [Metamath] Uncomfortable with definitions as axioms ... help?

The justification of definitions requires imposing additional structure on metamath databases in the form of being able to unambiguously parse statements into trees. Without it, you can't use the definition checker at all, and the rules do not make sense / could be circumvented without more rules.

Re: [Metamath] Uncomfortable with definitions as axioms ... help?

On Wed, Jul 12, 2023 at 4:35 AM Marshall Stoner wrote: > I trust that intuitively that these definitions are valid. The problem is > an alias rule can still fail if the syntax of the definition doesn't meet > certain criteria. If the parenthesis surrounding ↔ were missing in the > definition

Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

ilt up from those primitives, and then it is a short hop using theorems like ~sbie to get other forms of it involving explicit substitution, not free, alpha renaming, or other things. On Tue, Jul 4, 2023 at 2:10 AM Mario Carneiro wrote: > (This group is manually moderated, so posts may not appear immediately.)

Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

(This group is manually moderated, so posts may not appear immediately.) On Tue, Jul 4, 2023 at 2:04 AM Marshall Stoner wrote: > I wanted to share the pdf I've written so far but it didn't send and I > lost what I wrote. I guess attachments aren't allowed. I'll post a link > instead. > > pdf

Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

ended interpretation of the notation. If you think this documentation can be improved, we of course welcome any tweaks you would like to suggest.) Mario Carneiro -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe f

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

; functionality (like graph exports) to another command-line crate, > > - or splitting library and command-line tool, with the graph export > functionality moving to the command-line tool part? > > _ > Thierry > > > On 08/06/2023 19:40, Mario Carneiro wrote: > > I am

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

I am actually a bit concerned at the growth in behaviors of what is ostensibly a library. We need better separation between the proof assistant and the library, possibly a second crate in the same repo. On Thu, Jun 8, 2023 at 9:48 AM David A. Wheeler wrote: > > > > On Jun 5, 2023, at 8:48 AM,

Re: [Metamath] How are typecodes used/enforced by the Metamath program?

On Mon, Jun 5, 2023 at 1:43 AM Humanities Clinic wrote: > Hihi, I have read most of Dr Megill/Wheeler's Metamath book, as well as > most of the MPE pages, and I understand that typecodes are used to specify > the type of a variable in $f statements. > > (1) How and when does Metamath ensure the

Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions

The ∀푎 ∈ (Base‘푔) expression, or in ascii syntax "A. a e. (Base`g)" is the beginning of the restricted forall quantifier "A. x e. A ph" where you have highlighted just the "A. x e. A" part. It is read "for all x in A, ..." and denotes that some property "ph" holds for every x such that x e. A

Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html?

MM is already a "machine-readable" format, it is not much harder to parse than JSON (depending on what kind of information you are interested in), and you can even reasonably parse it with regexes, especially if you stick to MM files with a standard layout like set.mm. Your query about graph file

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

> Therefore there is a risk that official Metamath site suggests a tool which performs not so good as it has to and nobody knows that. I don't think this is a major concern, as long as we manage expectations on the landing page. Metamath and all associated tools come with no warranty, after all.

Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d

export, when the proof is complete it prints a big block of text, and I copy that block into the .mm file. On Wed, Apr 19, 2023 at 11:51 AM Mario Carneiro wrote: > You can use the "Renumber" option in the menu of mmj2 to get rid of "d" > and other alphabetic naming. The !

Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d

You can use the "Renumber" option in the menu of mmj2 to get rid of "d" and other alphabetic naming. The ! steps should also go away once you have proved the step, meaning that complete proofs will hopefully not have these things. * comments though are ubiquitous in mmj2 proof worksheets and I

Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style)

The most relevant theorem appears to be https://us.metamath.org/mpeuni/elnnz1.html . In general, you should try to look for biconditional statements as well, because we try to prove biconditionals when possible, and instead rely on versions of modus ponens that build in some kind of biconditional

Re: [Metamath] Reverse polish notation proofs from first principles exclusively

IIRC metamath.exe has a mechanism to show the length of such a proof, but not to calculate the proof itself. Note that these proofs get really ridiculously long (I think you need bignum arithmetic just to determine how many lines of proof there would be), so it's not practical outside toy

Re: [Metamath] Re: mmj2 compact representation for $d statements

Mario Carneiro wrote: > I recently implemented a variation on this algorithm for mm-web-rs: > https://github.com/digama0/mm-web-rs/blob/master/src/render.rs#L1026-L1077 > > As the function name suggests, the thing to google is "clique cover". It > is an NP hard problem

Re: [Metamath] Re: mmj2 compact representation for $d statements

I recently implemented a variation on this algorithm for mm-web-rs: https://github.com/digama0/mm-web-rs/blob/master/src/render.rs#L1026-L1077 As the function name suggests, the thing to google is "clique cover". It is an NP hard problem, but there are some okay approximations. On Sun, Apr 2,

Re: [Metamath] Negative use cases database?

The only source I am aware of is https://github.com/david-a-wheeler/metamath-test and the metamath-exe test suite (https://github.com/metamath/metamath-exe/tree/master/tests). Collecting failing tests and serving as a unit test for new verifiers is part of the stated purpose of the former

Re: [Metamath] Metamatix

The paper "models for metamath" (https://arxiv.org/abs/1601.07699) works out the requirements for models of metamath databases. They tend to be rather abstract as metamath is fairly logic-agnostic; you can get more useful models if you add some axioms to make it more like FOL specifically. If you

Re: [Metamath] mmj2 error js does not exist

Oops, you already sent the result. This is the nashorn error, same as for JDK 18+. On Sat, Mar 4, 2023 at 3:18 AM Mario Carneiro wrote: > That's the expected error when you run mmj2.jar without any arguments. Try > running the bash script now. > > On Sat, Mar 4, 2023 at 2:03 AM Will

Re: [Metamath] mmj2 error js does not exist

That's the expected error when you run mmj2.jar without any arguments. Try running the bash script now. On Sat, Mar 4, 2023 at 2:03 AM William Mitchell Jr wrote: > after apt install openjdk-17-jre, > > java --version: > openjdk 17.0.6 2023-01-17 > OpenJDK Runtime Environment (build

Re: [Metamath] mmj2 error js does not exist

(FYI you have to pass arguments to the jar file if you don't want it to immediately quit with an error message, this is why the bash wrapper exists. But the missing .so error seems to happen first.) Googling this seems to suggest that your JDK 17 installation is broken, try reinstalling it. Does

Re: [Metamath] mmj2 error js does not exist

This is the same error as before, you need to compile the java files using the same version as the one you use to run the jar file (in this case JDK 17). Since you are switching between versions it is likely you forgot to recompile and are using a class file from JDK 18+, as the error message

Re: [Metamath] mmj2 error js does not exist

what is the regular output? On Fri, Mar 3, 2023 at 11:21 PM William Mitchell Jr wrote: > Here is the output of strace java -jar mmj2/mmj2jar/mmj2.jar: > > https://pastebin.com/eMMHSGLs > > William > On Friday, March 3, 2023 at 10:26:40 PM UTC-5 di@gmail.com wrote: > >> The strace output is

Re: [Metamath] mmj2 error js does not exist

The strace output is not very informative because mmj2/mmj2jar/mmj2 is actually a shell script which calls java. Most of what you can see is just bash reading the script. You can call java directly if you want a more useful trace. On Fri, Mar 3, 2023 at 9:40 PM William Mitchell Jr wrote: > Here

Re: [Metamath] mmj2 error js does not exist

By the way, if you are thinking about modernizing mmj2 there are two known issues with newer versions of the JDK. One is the missing nashorn support as already mentioned, and the other is an issue in the undo system which causes ComposedEdits to not work correctly (the required class doesn't exist

Re: [Metamath] mmj2 error js does not exist

On Fri, Mar 3, 2023 at 5:41 PM William Mitchell Jr wrote: > openjdk-8-jdk: > Error: A JNI error has occurred, please check your installation and try > again > Exception in thread "main" java.lang.UnsupportedClassVersionError: > mmj/util/BatchFramework has been compiled by a more recent version

Re: [Metamath] mmj2 error js does not exist

:49 UTC David A. Wheeler wrote: > >> >> >> > On Mar 2, 2023, at 4:36 PM, Mario Carneiro wrote: >> > >> > It sounds like the nashorn JS engine was removed from a later version >> of JDK, and the empty list following the prompt suggests there is no >&

Re: [Metamath] Future website directions

> non-MathML case (just a little CSS), though I don't know how hard that is > for MathML/MathJax. > > > > On Mar 2, 2023, at 4:33 PM, Mario Carneiro wrote: > > This is a pretty fundamental problem with MathJax style displays, and I > don't have a good solution. LaTeX ge

Re: [Metamath] mmj2 error js does not exist

It sounds like the nashorn JS engine was removed from a later version of JDK, and the empty list following the prompt suggests there is no replacement. Without it you won't be able to run any macros, although you might be able to install it manually? The easiest thing to do is probably just to

Re: [Metamath] Future website directions

On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler wrote: > 2. The text just runs off to the right, instead of going over multiple > lines, making long ones unreadable. That's important but easy for the > non-MathML case (just a little CSS), though I don't know how hard that is > for

Re: [Metamath] Future website directions

n February 25, 2023 5:33:02 PM EST, Mario Carneiro > wrote: >> >> A page with short descriptions of papers and projects using Metamath for >> AI would be great to put on the website. I think it would be good publicity >> for both metamath and the AI systems,

Re: [Metamath] Future website directions

tamath site. >> > >> > With pre-rendering as a replacement for dynamic server side stuff, we >> can still do most of the things. For example we could prerender all the >> json queries and use client side JS to request them when doing cross >> linking stuff. This is

Re: [Metamath] Re: Formalizing Fermat's Last Theorem

I'm pretty sure the people who can edit wiki articles is the same as the set of people with write access to the set.mm repo. On Tue, Feb 21, 2023 at 12:02 AM Jim Kingdon wrote: > Oooh, thanks. I've been thinking a bit about formalizing n=3 or n=4 in > metamath (or perhaps more likely,

Re: [Metamath] Future website directions

On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler wrote: > > While yes I agree that this would be much better done with > metamath-knife than metamath-exe, I don't think there is a major concern > here, or at least we can mostly mitigate the issues since this flow is > extremely light on input

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

Oops, that was the wrong link, I meant to point to https://www.mediawiki.org/wiki/Page_Previews . (I investigated how this feature is implemented a while ago, with an eye for doing something similar for theorem references.) On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro wrote: > I don't

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

un, Feb 19, 2023 at 5:43 AM Antony Bartlett wrote: > On Sat, Feb 18, 2023 at 11:04 PM Mario Carneiro wrote: > >> Even if you have a highly optimized mm verifier, you can't get around the >> fact that you need to send some 30 MB over the wire before you can do >> anything.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

On Sat, Feb 18, 2023 at 5:16 PM David A. Wheeler wrote: > > > > On Feb 18, 2023, at 4:08 PM, Mario Carneiro wrote: > > In case it wasn't clear (and it probably wasn't), in a future world in > which the default mechanism is some super fancy client side renderer it is >

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

> > While I have some sympathy for this argument, I also think it is holding > us back a lot. Catering to the least common denominator of no-JS means that > our web pages are stuck permanently in web 1.0, with no search > functionality, intra-page links, subproof expansion, mathml rendering, >

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

> > I do see big downsides for the use cases listed here though: > 1. For training a GPT, I fear that the system would focus on "it's a JSON > file!" > and any tool-specific training would be swamped by thinking it's the same > as other JSON files. > I think a GPT system that trains on the

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

I think a json version of the web pages would make a lot more sense than a plain text version, if the intent is to support machine consumption by tools that can't parse metamath already. There are even uses for that in the web pages themselves, since an interactive version of the web pages would

Re: [Metamath] status of nnne0ALT

It sounds like we were unable to prevent a proof modification in this case. We'll have to go back through the history to find out what the original proof was and how it degenerated. On Wed, Feb 1, 2023 at 12:54 PM Zheng Fan wrote: > The proof of nnne0ALT is a thin wrapper of 0nnn, which is in

Re: [Metamath] Re: Should eliminate the GIF directories & just use Unicode?

I don't think the redirect would be that difficult, it is a one time apache configuration thing, possibly plus updates to the mirrors. On Mon, Jan 2, 2023 at 11:25 PM Jim Kingdon wrote: > There are a lot of ideas on this thread which might be worth doing, but > the redirect from mpegif to

Re: [Metamath] Should eliminate the GIF directories & just use Unicode?

I think it's not worth it to have ascii symbols in title attributes on every character. This will unnecessarily blow up the page size quite considerably. I think Benoit's suggestion of an all-ascii version of the pages is better - I think this is already implemented in one of the alternate

  1   2   3   4   5   >