I didn=E2=80=99t cover the linux issue in my last message. This is something I have no memory of. I think at the time I was working on the assumption that I would do the = work on MacOS and you would sort out any issues arising on other = platforms, and I certainly would not have liked to leave Linux hanging.
I only recently replaced my MacBook and at the time I had no intention = of doing any more development work. But within a small number of weeks I had completely changed how I was = thinking about the future, and re-instated software development to a = significant place. So I got the basic spec of the most recent MacBook, and almost = immediately found that I was going to need more space! I now also have a 2TB external SSD, so I think I should be able to = install a linux on there. However, first I had in mind trying out GitHub Copilot by seeing whether = it is congenial for ProofPower related developments, and in particular I = thought I would see whether it could help me tidy up the utf8 work I = did. Since I had negligible experience in coding in C at the time, and in = general coding is not my forte, its a mess, and doesn=E2=80=99t comply = with any imaginable coding standards (but seems to work). Quite possible that an AI assisted tidy up would eliminate the problems = being raised on Linux. I have forked pp because I have in mind doing things with the pp code = base which would not really belong there and so I was intending to do = something on a branch from utf8 on my fork to merge back into the pp = repo once complete. Other things I have in mind include decoupling the logical kernel from = the concrete representation of the theory store and concrete syntax in = general, and experimenting with the alpha zero method for non-LLM AI for = automation of theorem proving. I=E2=80=99m assuming that I will get increasingly valuable help from = LLMs and their derivatives in doing developments which I would otherwise = have thought infeasible. Already they save me huge amounts of time in discovering how to do = things on which I am clueless. So I am keen to find out how I will get on with GitHub Copilot, and that = will be best for the C development work, since Copilot seems to be = coupled to language tied support in VS code, and probably doesn=E2=80=99t = have SML support. (Though LLMs generally seem to think they do understand SML, so I = don=E2=80=99t know why I would need special support for Copilot to help = with it). Anyway, the bottom line is that I=E2=80=99m sorry to hear that pp on = Linux has been left behind on utf8 and will try and sort that out. Roger _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
