Company profile - Canadian Company Capabilities
Third-Party Information Liability Disclaimer
Some of the information on this Web page has been provided by external sources. The Government of Canada is not responsible for the accuracy, reliability or currency of the information supplied by external sources. Users wishing to rely upon this information should consult directly with the source of the information. Content provided by external sources is not subject to official languages, privacy and accessibility requirements.
Mind Alive Inc.
Mailing Address:
6716 75th St NWEDMONTON, Alberta
T6E 6T9
Location Address:
6716 75th St NWEDMONTON, Alberta
T6E 6T9
Tel.:<PHONE_NUMBER>
Tel.:<PHONE_NUMBER>
Fax:
Logo
Company Profile
Mind Alive Inc., an electronics manufacturing and
design company incorporated under the former name of Comptronic
Devices Ltd. in the province of Alberta in 1981,
designs and manufactures a series of mental and performance
enhancing products. Foremost are brainwave entrainment devices:
the DAVID series: Delight, Delight Plus, Delight Pro, SMART and ALERT.
These devices are used worldwide to assist people from all
walks of life to promote better health and assist in relaxation,
In addition, they have proven effective for many other
applications such as pain control, improving brain function,
increasing creativity, improving sports performance, and helping
to alleviate the symptoms of insomnia, PMS, Seasonal Affective
Disorder, Fibromyalgia, hypertension, and Attention
Deficit Disorder. This technology has gained popularity because
it has been proven to be a quick, yet safe and effective
alternative to many pharmaceutical approaches.
In 1985, Comptronic Devices Limited designed the first
D.A.V.I.D.1 (Digital Audio/Visual Integration Device) using
flashes of lights and pulses of tones to guide the user into
specific selected brainwave patterns through thalamic action.
They were originally used to enhance relaxation and meditation.
Since this time, Mind Alive Inc., through careful
market studies, university-based research and a well-developed
product research and development team, designed the DAVID series of devices. Their success is due to their portability, easy programmability and relatively low cost when compared to other treatment methods.
We are also proud of our reputation as leaders in this industry
by providing outstanding knowledge, quality and expertise for
our customers.
Presently, over 20 schools in Minnesota use our equipment to
help special needs children, particularly to help improve
attention & cognition while reducing behavioral problems such as
hyperactivity and belligerence. Dave Siever routinely lectures
at various conferences such as "The Association of Applied
Psychophysiology (AAPB), International Society for Neuronal
Regulation (ISNR) and Futurehealth Brain/Mind Conference, plus
other conferences.
Products Manufactured
Mind Alive Inc. offers the highest quality AVE devices
in the world: DAVID Delight, SMART and ALERT We also offer our
Cranio-electrical Stimulation (CES) device, the OASIS PRO, used to
enhance endorphin production.
Using advanced computer technology, along with the Soft-Off,
patented Tru-Vu Omniscreen eyesets and many other
features, the DAVIDs are now the most powerful, versatile
portable AVE devices available on the market today.
Our observations indicate that the quality of the AVE device
directly affects the quality of the user's experience and
results. Therefore, it is our commitment to provide products of
the highest quality.
Full profile
Full profile
Contact information
Company description
Product / Service / Licensing
in the area of reducing anxiety and improving cognition with
recovering alcoholics and drug addicts. There are also a few
studies showing reductions in anxiety and cognitive improvements
with the normal population. CES is officially recognized by the
FDA for the treatment of anxiety, pain and insomnia. Our
product, the Oasis, delivers a small electrical current via
disposable electrodes placed behind the ears. Can also be used for transcranial DC stimulation and micro TENS.
(1) Relaxation and Stress Management - The Digital Audio-Visual
Integration Device (DAVID) was originally developed in 1984. After several generations of AVE devices, we now offer the Delight series. Most of the sales are directed toward psychologists,
some medical doctors and their patients. The DAVIDs are very
effective in guiding the user to deep levels of relaxation and
general well-being. We have developed several Special
Application Sessions in conjunction with other brainwave
professionals to be used with the DAVIDs.
(2) Enhance Creativity - Many users of the DAVID believe that it
has helped them reach new levels of creativity.
(3) Sports Performance Enhancement - Bodybuilder Frank Zane
"I'm in the best shape of my life, and one reason is mind
machines."; Golfer Rocky Thompson attributes his winning of the
PGA to using the Paradise; Sports Psychologist Tom Hawes has
used the Paradise in training several women in the LPGA. We
offer a Special Application Session developed with MindAerobics,
Wisconsin to assist the user to effectively tap into his/her
potential to strengthen the mind to get the most out of physical
abilities.
(4) Pain Reduction - The DAVID has been used by many clinicians
and doctors to assist their patients in the management of
chronic pain. In 1992, "The Use of Repetitive Audiovisual
Entrainment in the Management of Chronic Pain" by Dr. Frederic
Boersma, Ph.D. was published in the Medical Hypnoanalysis
Journal reporting strong positive effects associated with
treatment, reduced medication usage, decreased stress and
greater restfulness in sleep.
(5) Attention Deficit Disorder - Research has been
conducted to determine the effectiveness of using the DAVID to
treat ADD/ADHD. Anecdotal studies indicate that after using
this technology, many people can reduce or quit their dosage of
Ritalin and learn to manage their ADD symptoms.
We are currently conducting research projects on the
effectiveness of light and sound stimulation in the treatment of
chronic pain, insomnia and Attention Deficit Disorder.
Mind Alive Inc. continues to research and develop new
products. Our products are all thoroughly tested for durability,
reliability and effectiveness.
At Mind Alive Inc. it is our commitment to provide our
customers with superior products that promote a healthier and
higher quality of life. We are also committed to providing
exceptional customer service.
The DAVID Delight series of AVE devices are the most
versatile and powerful portable light and sound stimulation
device on the market today. We have combined many years of
market research and product development to offer you the
features and benefits not seen on any other light
and sound stimulation device. Some of these features are
extremely important to ensure the effectiveness of the DAVIDs
as a tool to assist in your quest to heightened states of
consciousness and awareness.
Like the well known principles of resonance which are necessary
for one tuning fork to transfer its vibration to another, the
same "rules" or principles must be present for brainwave
entrainment to occur. Brainwaves change frequencies based on
neural activity within the neural functions of the brain. The
senses of vision, touch, smell, taste and hearing provide for
access to the neural functions of the brain. Each of these
senses responds to activity within the environment and transmits
the information to the brain. The senses of sight and hearing
by their very nature, provide a fertile medium for entrainment
of brainwaves, and therefore, production of various and
beneficial states of consciousness.
In order that the DAVID can be an effective entrainment
device, we strive to ensure that the DAVIDs comply with the rule of entrainment:
The Power Rule - The stimulus must be powerful enough to
elicit a sufficient response in the visual and auditory cortexes
of the brain at any brain wave frequency.
The Oasis Pro is used to enhance relaxation, aid with sleep, improve mood using Cranio-electrical stimulation.
symptoms of depression, anxiety, attentional disorders,
hypertension, Seasonal Affective Disorder, PMS, chronic pain,
Fibromyalgia, insomnia, and to enhance sports and cognitive
performance. AVE does this by increasing cerebral flow
(improving cognition) and by dissociating a person out of
sympathetic (fight or flight) responses. It has been used to
reduce the effects of PTSD and is used by many
soldiers and veterans. AVE is used by many
psychologists, chiropractors, massage therapists,hypnotherapists
and an increasing number of professional athletes (Christine Boudrais
attributed her 1994 Olympic silver medal to using our DAVID
AVE system).
Market profile
Alliances:
- Sales/Marketing
Geographic markets:
Export experience:
- Algeria
- Australia
- Belgium
- Brazil
- France
- Germany
- Hong Kong
- Hungary
- Japan
- Luxembourg
- Netherlands
- New Zealand
- Philippines
- Russian Federation
- United Kingdom
- United States
- Venezuela, Bolivarian Republic of
- California
- Florida
- Georgia
- Maryland
- Massachusetts
- Michigan
- New York
- Ohio
- Pennsylvania
- Texas
- Washington
Actively pursuing:
- Iran, Islamic Republic of
- Spain
- Alabama
- Alaska
- Arizona
- Arkansas
- Colorado
- Connecticut
- Delaware
- District of Columbia
- Hawaii
- Idaho
- Illinois
- Indiana
- Iowa
- Kansas
- Kentucky
- Louisiana
- Maine
- Minnesota
- Mississippi
- Missouri
- Montana
- Nebraska
- Nevada
- New Hampshire
- New Jersey
- New Mexico
- North Carolina
- North Dakota
- Oklahoma
- Oregon
- Rhode Island
- South Carolina
- South Dakota
- Tennessee
- Utah
- Vermont
- Virginia
- West Virginia
- Wisconsin
- Wyoming
Third-Party Information Liability Disclaimer
Some of the information on this Web page has been provided by external sources. The Government of Canada is not responsible for the accuracy, reliability or currency of the information supplied by external sources. Users wishing to rely upon this information should consult directly with the source of the information. Content provided by external sources is not subject to official languages, privacy and accessibility requirements.
Contacts
Contact information
Description
Company description
Products, services and licensing
Product / Service / Licensing
in the area of reducing anxiety and improving cognition with
recovering alcoholics and drug addicts. There are also a few
studies showing reductions in anxiety and cognitive improvements
with the normal population. CES is officially recognized by the
FDA for the treatment of anxiety, pain and insomnia. Our
product, the Oasis, delivers a small electrical current via
disposable electrodes placed behind the ears. Can also be used for transcranial DC stimulation and micro TENS.
(1) Relaxation and Stress Management - The Digital Audio-Visual
Integration Device (DAVID) was originally developed in 1984. After several generations of AVE devices, we now offer the Delight series. Most of the sales are directed toward psychologists,
some medical doctors and their patients. The DAVIDs are very
effective in guiding the user to deep levels of relaxation and
general well-being. We have developed several Special
Application Sessions in conjunction with other brainwave
professionals to be used with the DAVIDs.
(2) Enhance Creativity - Many users of the DAVID believe that it
has helped them reach new levels of creativity.
(3) Sports Performance Enhancement - Bodybuilder Frank Zane
"I'm in the best shape of my life, and one reason is mind
machines."; Golfer Rocky Thompson attributes his winning of the
PGA to using the Paradise; Sports Psychologist Tom Hawes has
used the Paradise in training several women in the LPGA. We
offer a Special Application Session developed with MindAerobics,
Wisconsin to assist the user to effectively tap into his/her
potential to strengthen the mind to get the most out of physical
abilities.
(4) Pain Reduction - The DAVID has been used by many clinicians
and doctors to assist their patients in the management of
chronic pain. In 1992, "The Use of Repetitive Audiovisual
Entrainment in the Management of Chronic Pain" by Dr. Frederic
Boersma, Ph.D. was published in the Medical Hypnoanalysis
Journal reporting strong positive effects associated with
treatment, reduced medication usage, decreased stress and
greater restfulness in sleep.
(5) Attention Deficit Disorder - Research has been
conducted to determine the effectiveness of using the DAVID to
treat ADD/ADHD. Anecdotal studies indicate that after using
this technology, many people can reduce or quit their dosage of
Ritalin and learn to manage their ADD symptoms.
We are currently conducting research projects on the
effectiveness of light and sound stimulation in the treatment of
chronic pain, insomnia and Attention Deficit Disorder.
Mind Alive Inc. continues to research and develop new
products. Our products are all thoroughly tested for durability,
reliability and effectiveness.
At Mind Alive Inc. it is our commitment to provide our
customers with superior products that promote a healthier and
higher quality of life. We are also committed to providing
exceptional customer service.
The DAVID Delight series of AVE devices are the most
versatile and powerful portable light and sound stimulation
device on the market today. We have combined many years of
market research and product development to offer you the
features and benefits not seen on any other light
and sound stimulation device. Some of these features are
extremely important to ensure the effectiveness of the DAVIDs
as a tool to assist in your quest to heightened states of
consciousness and awareness.
Like the well known principles of resonance which are necessary
for one tuning fork to transfer its vibration to another, the
same "rules" or principles must be present for brainwave
entrainment to occur. Brainwaves change frequencies based on
neural activity within the neural functions of the brain. The
senses of vision, touch, smell, taste and hearing provide for
access to the neural functions of the brain. Each of these
senses responds to activity within the environment and transmits
the information to the brain. The senses of sight and hearing
by their very nature, provide a fertile medium for entrainment
of brainwaves, and therefore, production of various and
beneficial states of consciousness.
In order that the DAVID can be an effective entrainment
device, we strive to ensure that the DAVIDs comply with the rule of entrainment:
The Power Rule - The stimulus must be powerful enough to
elicit a sufficient response in the visual and auditory cortexes
of the brain at any brain wave frequency.
The Oasis Pro is used to enhance relaxation, aid with sleep, improve mood using Cranio-electrical stimulation.
symptoms of depression, anxiety, attentional disorders,
hypertension, Seasonal Affective Disorder, PMS, chronic pain,
Fibromyalgia, insomnia, and to enhance sports and cognitive
performance. AVE does this by increasing cerebral flow
(improving cognition) and by dissociating a person out of
sympathetic (fight or flight) responses. It has been used to
reduce the effects of PTSD and is used by many
soldiers and veterans. AVE is used by many
psychologists, chiropractors, massage therapists,hypnotherapists
and an increasing number of professional athletes (Christine Boudrais
attributed her 1994 Olympic silver medal to using our DAVID
AVE system).
Market
Market profile
Alliances:
- Sales/Marketing
Geographic markets:
Export experience:
- Algeria
- Australia
- Belgium
- Brazil
- France
- Germany
- Hong Kong
- Hungary
- Japan
- Luxembourg
- Netherlands
- New Zealand
- Philippines
- Russian Federation
- United Kingdom
- United States
- Venezuela, Bolivarian Republic of
- California
- Florida
- Georgia
- Maryland
- Massachusetts
- Michigan
- New York
- Ohio
- Pennsylvania
- Texas
- Washington
Actively pursuing:
- Iran, Islamic Republic of
- Spain
- Alabama
- Alaska
- Arizona
- Arkansas
- Colorado
- Connecticut
- Delaware
- District of Columbia
- Hawaii
- Idaho
- Illinois
- Indiana
- Iowa
- Kansas
- Kentucky
- Louisiana
- Maine
- Minnesota
- Mississippi
- Missouri
- Montana
- Nebraska
- Nevada
- New Hampshire
- New Jersey
- New Mexico
- North Carolina
- North Dakota
- Oklahoma
- Oregon
- Rhode Island
- South Carolina
- South Dakota
- Tennessee
- Utah
- Vermont
- Virginia
- West Virginia
- Wisconsin
- Wyoming


Guidance
How schools and local authorities access and use the service.
Ref: DFE-00610-2014 PDF , 3.82MB , 21 pages
Ref: DFE-00609-2014 PDF , 2.15MB , 25 pages
Ref: DFE-00205-2016 PDF , 892KB , 13 pages
PDF , 259KB , 2 pages
Guidance on how to use the S2S secure data transfer system to send pupil data using the common transfer file to schools and local authorities.
The guides cover:
Published: 10 December 2013
Updated: 2 October 2014
From: Department for Education


Regulators begin probe into Google-Ascension cloud computing deal: WSJ
(Reuters) - A U.S. federal regulator has initiated an investigation into a cloud computing deal between Alphabet Inc’s Google and Ascension Health [ASCNH.UL] which would give Google access to detailed health information of millions of patients, the Wall Street Journal reported on Tuesday.
The Office for Civil Rights in the Department of Health and Human Services will look into the data collection to ensure the partnership is in compliance with the Health Insurance Portability and Accountability Act (HIPAA) which safeguards medical information, the Journal said on.wsj.com/2NGPPQX.
On Monday, Google said patient data “cannot and will not be combined with any Google consumer data.”
Google did not immediately reply to Reuters’ request for comment.
(This story corrects abbreviation in second paragraph to HIPAA)


--- layout: archive title: Zulip Chat Archive permalink: /stream/113488-general/topic/markdown.20module.20docstrings.html ---
Noob question.
Since we're writing all these docstrings at the top of .lean
files in mathlib in markdown, presumably there's an easy way to see the markdown? What does /-! -/
do?
Nothing useful with Lean 3.4.2 -- I think there's something missing from the API that's either fixed or fixable in the community fork. They're docstrings associated with the file instead of a particular declaration, and metaprograms can in principle access them.
IIRC in 3.4.2 you can only get the docstring for the current file.
It's more of a future-proofing thing. At some point we'll want to generate HTML docs for the library, and having the comments already in markdown will be convenient then.
It might actually be a useful VSCode plugin to format and display the module doc for the current file when you press a button.
You can see lean 3.4.2's tests doc_string3.lean for the extent of the non-community edition support e.g. there are some tactics for printing out the doc_strings.
I haven't tested if lumpy-leandoc does the right thing for /-! -/
yet (edit: it should work)... but it'd be very easy to add something which extracts the .md file to it in addition to the limited html/pdf stuff it currently does.
@Chris Hughes I fixed up lumpy so it could build mathlib again, mathlib-docs.zip
Rob Lewis seems correct in that it's not useful with 3.4.2 in lumpy at least, the /-! -/
comments never make it to the output, so /-! -/
only shows up when the lean files were built with the community edition.
The way lumpy treats /-! -/
is to include it verbatim, i.e. It doesn't prepend it with the name of the definition to which the doc_string is associated, because it's generally just associated with the section that corresponds to the file.
Hopefully that helps.
That's actually closer to real doc generation than I realized we were.
It seems to be treating the sections of module docs as sections of the document, which is very confusing.
But the core structure is there.
It seems to be treating the sections of module docs as sections of the document, which is very confusing.
In the PDF, that is. The HTML looks better, except it doesn't print the def names? Which do appear in the PDF?
Yeah, it's because I was following the html -> tex convention that e.g.
 corresponds to \chapter
 \section etc, and the docs aren't really built with that in mind
Yeah, this was the forseeable problem with creating the doc standards before we could generate docs.
Yup, I haven't done a lot of work on the html generation (or in fact looked at it today), it should in theory be easy to add unless i have forgotten why it is missing, I will try and look at it again tomorrow and fix that if I can.
Cool. What are the prospects for linking? Something like this: "if an identifier appears between backticks, and we've seen a declaration with that name, turn it into a link." I'm guessing that's way more work?
Something like that, It'll need some thought, as it parses all lean files in parallel currently, so i'll probably have to do a pass over declarations build a table of declarations first before generating links (I'm guessing we want to link across files, which means we also need to mirror the import behavior I suppose)... :octopus:
With two passes I think you could ignore the import tree. Generate a table the first pass, and note which html file each declaration will live in. Then fill in the info in the second pass. Namespacing means this will be impossible to get exactly right though. There's no way doc strings will be consistent about referring to declarations with full namespaces, and there will be ambiguous cases.
yeah, shall see if we can get away with that, anyhow i must get going.
Thanks for looking into this! It would be great to generate HTML docs for the website and this isn't so far off.
Well, i updated it (and the zip file) to add the names of declarations, and a horizontal rule separating the header.
I think i will look at making TeX rendering optional, because the output isn't ready for consumption and it makes integrating into CI difficult since it needs lots of font stuff compiled in a specific way... With that it'll hopefully be easier to integrate into the website...
Nice! I just checked out a couple of the better documented files. It looks great. https://leanprover-community.github.io/doc_demo/manifold.html
What about printing the type of the declaration along with the name?
Right now it only prints declarations that have docstrings, right? Our doc guidelines don't require them for theorems, since in principle all you need to know about a theorem is its statement. Complicated/big/important theorems should have docstrings anyway, but we probably want more than just those in the doc output.
Is it overkill to print everything in the html docs? It feels to me like it should describe a "public" API, and there are plenty of things in the library that don't need to show up there. But I'm not sure.
@matt rice Wow, that looks really good
The

s containing the declarations should have a class so we can style it better, but that's easy.
Also we need index pages. Also easy, I hope :)
Once this is up and running, it gives another argument for a mathlib release schedule. We could update the docs daily. But it would probably be clearer to have fixed versions.
I will look at printing the type declaration, it's been on my list of things to do, but I have been scared that it's just going to give me the thing that the type is definitionally equal to, since i'm pulling it out of the bytecode :D
I don't know anything about html really, i'll try and figure out the div's class, I assume i need to declare some empty style e.g. decl and then give it the class decl?
I also wish I could style the syntax highlighting rather than hard coded colors, but that is going to take some work.
For the div classes, the easy part is printing

instead of just

. Then someone needs to add a css file that styles them properly, which we probably want to integrate with the rest of the website.
I suspect you'll get a presentable type, but I don't know.
index should be easy it's already in a big table just need to enumerate the keys of.
Can you use pygments to generate highlighted code?
it's currently using syntect with a conversion of the vscode syntax highlighting, I haven't really compared to how vscode gets highlighted yet to see if that conversion is accurate though.
Using pygments would be a big change. Part of the reason i chose syntect is so i can compile the whole thing to web assembly eventually and not shell out to stuff.
Aha... pandoc
uses pygments, and so does Zulip. I don't know syntect.
For the syntax highlighting, we could at least move the style definition to a separate css file, so the colors are specified once instead of every time code is displayed.
The Zulip archive lets Zulip do the structuring (with pygments, I think?) and then copies the Zulip CSS to display it.
I don't know how different the syntect structuring is, presumably it's not compatible. But we should be able to manually match the colors for analogous items.
Yeah, the problem is the syntax highlighter hard coding the colors, the current solution to this is to hard code the colors for each thing to a specific unique value and then sniff the colors and turn them into the appropriate CSS. Ideally I would like to just get it to emit CSS directly.
Oh, I see. That's kind of annoying.
Yeah, there should be a way to do it, but this was easy to add as a placeholder for now.
It's maybe not ideal, but it looks fine as-is. I wouldn't worry about it too much.
Nice! I just checked out a couple of the better documented files. It looks great. https://leanprover-community.github.io/doc_demo/manifold.html
Updated to apply the default stylesheet. Not bad, hmm?
The main thing that had me tearing my hair out with pygments was that each backend has different supported rendering options, like line numbers, and things So like html may support line-numbers and latex ignore them and what not. Eventually i would like to be able to attach footnotes to lines-numbers and for that I need some fairly custom syntax highlighting anyways.
Speaking of line numbers, does the Lean byte code let you access the line number of a declaration? Linking declarations to their statement on GitHub would be really nice.
Right now it only prints declarations that have docstrings, right? Our doc guidelines don't require them for theorems, since in principle all you need to know about a theorem is its statement. Complicated/big/important theorems should have docstrings anyway, but we probably want more than just those in the doc output.
I think that maybe we should only print things that do have a docstring. Otherwise it becomes close to replicating the source. These pages could be a good intermediate step that extracts the "juicy" bits.
Then I think we need to raise the percentage of theorems that get documented. The Python docs wouldn't be very helpful if they only told you the juicy parts about manipulating strings.
In principle the module docs at the top should point to the juicy bits.
So what is the purpose of these documents over the github source (besides typesetting the markdown)?
Omitting declaration bodies gets you pretty far from the source.
Imagine if the Python docs showed you the implementation of every function.
Yeah, you can extract line numbers, olean-rs/types.rs PosInfo structure. We should be able to make links revision-stable as well if we can pull the sha out of git.
But again, I'm not sure that every theorem deserves to show up in the HTML. Maybe we could use a @[nodoc]
attribute to make it opt-out instead of opt-in. We should have access to attributes from the byte code, right?
I believe so looks like either Modification::UserAttribute or Modification::Attr. let me know what you guys decide, currently I just ignore undocumented things.
Anyhow, going go try and implement some of the things discussed.
Hmm, a tougher one, can you identify when declarations are builtin or user-defined? We have a tactic to do this. But that might not be contained in the byte code.
We don't want to include random recursors and aux definitions in the docs.
I'm not sure, there has been plenty to do without getting too in depth with the bytecode so far :)
Hah, fair enough!
It seems that most (all?) Lean-generated definitions have a name starting with an underscore at some point in the namespace - _main
, _sunfold
, _eqn_n
. In addition, Lean rejects identifiers starting with the underscore, since these are reserved for the system, so it might suffice to just look for those in the name.
The things that come along with an inductive type don't. rec_on
, no_confusion
, etc.
Of course, it's easy enough to blacklist those.
There is a pretty comprehensive autogenerated definition check in the linter
But if we're extracting things with olean-rs we can't run that check.
Maybe the check could be reimplemented.
An issue with printing types is that olean files seem to contain them in raw form. Unless I'm missing something, pretty-printing would then require processing all notation and pretty much reimplementing the pretty-printer. As an alternative, we could query the Lean server for types of things from lumpy. This might be quite slow unfortunately.
updated the docs again, to include index and the css stuff. mathlib-docs.zip, I find the alphabetical order on directory/file mix bothersome, but it functions.
Maybe there's a better approach to this. Instead of extracting info directly from the oleans, should we do a first pass with a Lean metaprogram? That way we can use the existing autogenerated check, pretty-print types, etc.
We'd just fold over the environment and for each declaration export the name, type, file location, docstring, and any attributes we want to display. The export can be in whatever format is convenient for the formatter to parse.
One thing you can't get from this approach is info about file imports. I guess we'd want to print that at some point.
Yes, that is the approach I think we should take. Instead of a metaprogram though, I've hacked on Lean a bit to make it produce the list of declarations in each .lean file, as well as the top-level docstrings for it. Re. file imports, I'm not sure about tactic mode, but they should be obtainable from module_info
in the c++.
Ah, cool. Does it produce the list at the time the file is compiled, or after the whole build is done? If we want to print attributes, it's important to generate this at the end. If a declaration gets tagged as a simp lemma in a later file than where it's declared, we need to catch that.
It produces the list using the environment that exists at the last line of the file being compiled. Note that we cannot know a priori all places where a lemma is tagged as simp, just as we cannot know a priori all instances of a type class. For this reason, I would say that such tags should be documented in the module in which they exist rather than at the point where the to-be-tagged-simp lemma is declared. Same goes for typeclass instances. We could aggregate them after processing all of mathlib and then retroactively add forward-links, but that wouldn't extend to a general notion of package and would be more of a hack.
By the way, while for typeclasses this makes perfect sense, the design choice of allowing lemmas to be tagged as simp
after they are declared seems to only make sense if a lemma can be locally-simp, i.e. a useful simplification in the context of some theory, but maybe not generally. I'm not sure if this happens in mathlib but it seems plausible.
Oh, and because the signature of module_doc_strings : tactic (list (option name × string))
is weird, I am considering deleting it and replacing with module_doc_string : string -> string
, which returns the module doc string for the module identified by hopefully same scheme as in import
, e.g. module_doc_string ".mymod"
should return the doc for ./import.lean
. The declaration docs are still retrievable by folding over the environment, so no expressivity is lost.
I think, in general, we add attributes as soon as they're available. But this isn't always in the file where the declaration is defined: see e.g. the bottom of norm_cast
. It intuitively seems useful to document that int.coe_nat_succ
is a move_cast
lemma. That is indeed some kind of forward reference, but I'm not sure that's a problem for this kind of documentation. It's documenting the library as a whole, forward references aren't necessarily wrong. But it does seem wrong when an attribute is added deep in the file hierarchy. Declaring nat.prime
as a class in the p-adics files is an example of this, but there are also other reasons this shouldn't happen and WIP to change it.
Besides tactic attributes like move_cast
, ext
, etc, there aren't many cases where global attributes are added long after the declarations are defined. There are some reducibility level changes I think.
Oh, and because the signature of
module_doc_strings : tactic (list (option name × string))
is weird, I am considering deleting it and replacing withmodule_doc_string : string -> string
, which returns the module doc string for the module identified by hopefully same scheme as inimport
, e.g.module_doc_string ".mymod"
should return the doc for./import.lean
. The declaration docs are still retrievable by folding over the environment, so no expressivity is lost.
Coming back to this: what would be best (for me) is a function that returns a list of pairs (file, docs)
, where file
is a string that identifies a Lean file and docs
is the list of module doc strings for that file. (By module doc strings, I mean the file-level ones, not the ones associated with a declaration.)
As far as I can tell, there's still no way within Lean to get a module doc string from outside the current file. You're storing it in the oleans now, but it's not accessible by a metaprogram yet, right?
I spent a little too long doing this this afternoon, and it's clearly still rough. Here are mathlib docs generated by a combination of metaprogramming and Python: http://robertylewis.com/mathlib_docs/
Essentially, it folds through the environment and writes a json file with the info needed to display. A Python script formats it and tries to link identifiers that it finds in code blocks. Right now, the Python script scrapes module docs from the Lean source files. This will be cleaner if/when they're accessible with a metaprogram.
The formatting is modular. If it's better to produce the data from C++ or olean-rs or whatever, that works too.
This is completely awesome!
Rob, did you put the code somewhere? How can we help? We definitely need some CSS work.
I left the office without pushing it anywhere, but I'll make it available tomorrow. If you want to work on the CSS, you could work on a single file as an example.
The code is almost certainly not Windows friendly.
Who cares?
And scraping the module docs from source is really ugly. It will be more portable if we can avoid that.
Well, me when I'm at home working on my laptop...
You could also try to think of a way to linkify notation. There's not a general solution, since notation can reference more than one declaration, so there's no unique place to link it to. But it looks wrong to have ℕ
not be a link.
The first easy thing to do is to filter out _inst_. :
.
That's hopeless if we're using a metaprogram to generate the data, but @Wojciech Nawrocki or @matt rice 's approaches might be able to do more.
We really need Lean to cooperate here
Could all of this be easier as an extension of Lean 3.5.c?
With small changes to 3.5 I think we could avoid scraping the module docs from the source, at least.
Even if we don't switch mathlib over to lean 3.5.c, we could still use 3.5.c to generate the docs
Lean 3.5 can already build mathlib, right? So adding stuff that would make documentation easier seems like a very good idea.
Yeah, of course. Wojciech has already been working on the module doc API there.
As far as I can tell, there's still no way within Lean to get a module doc string from outside the current file. You're storing it in the oleans now, but it's not accessible by a metaprogram yet, right?
This is correct. I have a local branch in which they're accessible from C++ - I could add a tactic that exposes this storage.
The generated html is not well-formed and lacks classes, so working on CSS is not yet possible (but there is no hurry of course).
@Rob Lewis Just wanted to note that there is a branch on lumpy json-input for trying out Wojciech's approach in lumpy, I haven't got it using any of the additional information accessible yet, but i'll probably migrate to that if it works out.
Another formatting thing that might be nice: instead of printing the name above and the full type below, we could bind variables with the name. So instead of
iff_of_eq ∀ {a b : Prop}, a = b → (a ↔ b)
we'd have
iff_of_eq {a b : Prop} (h : a = b) (a ↔ b)
This would take some experimenting to get the formatting right. The identifier needs to stand out.
In fact, I also have something that sounds like your JSON generation. hensel.json is an example. It kind of works but performance is really bad as of now, so I'd like to fix that before PRing to lean 3.5. There is also all the internally-generated noise (_private.1428265847.newton_seq_dist_tendsto'
) which I didn't try to do anything about just yet.
@Rob Lewis does this JSON look similar to what you were exporting?
@matt rice also has a branch of lumpy-leandoc which can parse the JSON
Yeah, same idea, slightly different structure, but it would be easy to convert.
For the internal stuff, there are some meta defs that filter it that we use in the linter.
They could probably be replicated in C++.
Because I don't know anything about this black magic going on in this thread I've only half been paying attention. But several people have been in touch with me (because of natnumgame) asking me what maths Lean now has, what maths it needs etc. I am currently pouring all my Lean time into constructing a challenging inequality world for nng but once that's done I was thinking of a blog post of the form "hey, here's what we have now [list of stuff] and here's what we would like [list of other stuff]. I thought I'd mention this here because I was wondering if I could somehow integrate this list into the story somehow, e.g. "for more about groups, see this link here".
Puny initial attempt of "what we need" is here: https://github.com/kbuzzard/xena/blob/795563bfab087fc8cd8e23107fae43dc78b7b46e/100mathchallenges.txt (completely unfinished, the result of a number theoretic brain-dump).
Maybe the "theories" docs could be updated / reworked as well?
Of course it should be updated. And maybe the we should bring it closer to the Lean file, and put it on the same website, with links to the "per Lean file webpages".
I'm not sure we should rush to make the html docs public. This kind of thing works better with fixed releases of mathlib. Having it constantly update makes it harder to link to and harder for Google to index.
That said, it's not a huge deal if we put up a draft version soon-ish.
A lot of the md files in mathlib would be better converted to html and put on the community webpage.
Kevin's list would fit there too, if he wants it to be less Kevin and more mathlib.
I could easily allow lumpy to read .md as well as lean and just do a straight html conversion
I could easily allow lumpy to read .md as well as lean and just do a straight html conversion
For static pages (that aren't generated from the library), it's not necessary. We already use Jekyll to generate the site. Stick the right header on the md file and it will fit right in, styled and everything.
For things like the tactic docs that change a lot, maybe incorporating them into the doc generation would be good.
81 should do what you need.
Rob, did you put the code somewhere? How can we help? We definitely need some CSS work.
https://github.com/robertylewis/doc_gen/
It generates valid html now, and colors declarations based on whether they're theorems, defs, etc.
One more update for now. I should stop wasting time on this.
http://robertylewis.com/mathlib_docs/linear_algebra/basis.html
It looks like we'll have to be careful now about making sure that module docs and docstrings render well. The second wikipedia URL at the top of ring_theory/maps has underscores which are interpreted as markdown.
Yeah, there are tons of problems. It's hard to get it correct without seeing the end results. A lot more needs to be enclosed in backticks.
It looks like we'll have to be careful now about making sure that module docs and docstrings render well. The second wikipedia URL at the top of ring_theory/maps has underscores which are interpreted as markdown.
I managed to fix this and some mangled lists by passing the right options to the markdown formatter.
Unfortunately there doesn't seem to be an option to turn the urls into links.
Would it be unreasonnable to write markdown urls in Lean file?
That seems totally reasonable.
I'm pretty sure there are currently very few of them, and they are very easy to find.
So we could easily switch.
Yeah. I think we're going to find tons of things that need to be fixed. The mistakes become obvious once you actually parse the markdown.
So, I'm reaching a point where I'm kind of happy with the layout/CSS. Comments are welcome. https://robertylewis.com/mathlib_docs//geometry/manifold/smooth_manifold_with_corners.html
Declaration names link to the corresponding line on GitHub.
Are you color-blind? I'm asking out of curiosity.
What? No, it's a random color palette some website gave me.
We need a web designer.
The pink does jump out a little too much.
Yes, the pink in particular.
And it does feel old too.
And I think keeping the keywords def
, lemma
etc. would help.
I should have first written that the current result is already amazing!
You're welcome to suggest alternate colors!
And I think keeping the keywords
def
,lemma
etc. would help.
Oh, yeah, I meant to do this. I don't think there's any way to distinguish lemma/theorem, so we'd need to pick one.
It gets a little complicated with structures and inductives, because those are "constants" in the environment. But it should be possible to identify that.
It would be nice to use LaTeX in module docstrings when not quoting Lean code.
It's easy enough to support MathJax.
Is there a link to the GitHub page of the file somewhere? (I know there are links to individual declarations, although they come as a surprise).
It's kind of a minefield though
We should also think about having a responsive layout, for small screen browsing.
Is there a link to the GitHub page of the file somewhere? (I know there are links to individual declarations, although they come as a surprise).
No, where would you suggest adding it?
Somewhere at the top probably.
Maybe even h1 could be a link.
I've been leaning towards something like dvisvgm in lumpy which can convert pretty much any old tex to svg
What I did for my masters thesis was to basically rip off Rust's CSS, which gave me a nice basic layout without any effort on my side...
It's kind of a minefield though
I don't know much about it. We can add hooks in the markdown processing that capture $$ ... $$
blocks. That's as far as I got.
But I don't want to distract you from polya
, I shouldn't be writing those comments, and try to find time to try something on my side.
Maybe even h1 could be a link.
This is slightly tricky actually. The entire top block is the module doc from the Lean file. It's much easier to add things around it than inside it.
Sebastian is right, I'm sure we can steal ideas without hiring a web designer.
Yeah, I'm not very interested in making major design changes myself. If someone else wants to reformat I'm very happy to let them.
It's kind of a minefield though
I don't know much about it. We can add hooks in the markdown processing that capture
$$ ... $$
blocks. That's as far as I got.
Yeah I think the hard part is that each markdown tool supports variations on a similar syntax, but somehow they all manage to be different
and there is no standard to be found anywhere. here is a breakdown someone did mathdown
Maybe even h1 could be a link.
Oh, most files don't even have an h1 because there's no module doc. I'll add a "View file source" link in the navigation panel instead.
Yeah I think the hard part is that each markdown tool supports variations on a similar syntax, but somehow they all manage to be different
Right now I'm using the markdown2 library for Python which I don't think supports anything. But I can extract the raw text and feed it somewhere else for processing.
Again, in principle, I haven't actually looked into it yet.
@Rob Lewis about your suggestion in 81, If we added h2 to those groupings and had links for those too,
And since there's almost no LaTeX in md blocks right now, I don't think it's a priority!
With mathjax you only need to make sure LaTeX parts are untouched.
Rob Lewis about your suggestion in 81, If we added h2 to those groupings and had links for those too,
Yeah, we could build a TOC and put it after the header block if there are any subsections to link to.
nod my markdown parser doesn't handle them either (well, it refuses until there is a standard).
i've been using e.g.
```latex ``` and ```math ```
a bit verbose...
Anyhow, I know Rob's is a lot nicer, but set up a page with the current index generation here: doc_preview
The problem with mathjax/katex is that they both have absolutely zero support for diagrams, so if category theorists wanted to draw something with TikZ, it wouldn't work. Dvisvgm does support that, but requires offline generation of svgs.
Alright. Another update, with better support for structures/inductives, printing def/lemma/etc, and a few more tweaks. https://robertylewis.com/mathlib_docs/geometry/manifold/manifold.html
The code is now more or less portable. https://github.com/robertylewis/doc_gen
update-mathlib
isn't working when I try to do this locally. It says it succeeds, but then Lean wants to compile all of mathlib, even if I touch all the oleans first.
So if you try to install it you might need to do a full compile or get the oleans from elsewhere. Or maybe it's an issue on my end.
The problem with mathjax/katex is that they both have absolutely zero support for diagrams, so if category theorists wanted to draw something with TikZ, it wouldn't work. Dvisvgm does support that, but requires offline generation of svgs.
Absolutely zero support for diagrams is a little strong, https://github.com/sonoisa/XyJax does exist for mathjax and I've used it for many years as has the stacks project (https://stacks.math.columbia.edu/tag/0BW7), it is basically unsupported officially though and might even be broken with mathjax 3.0.
I don't think we should encourage people to use xypic
in 2019. Accepting tikz-cd with server-side rendering seems much wiser.
I just found a project to render Tikz in the browser with WebAssembly: https://github.com/kisonecat/tikzjax
I'm not encouraging, simply stating the facts that it is possible with client-side js
This tikz project seems very cool though!
Ah sorry, I meant "out-of-the-box support". Tikzjax certainly looks interesting, but I would question its stability - reloading a coredump of the entire TeX compiler in the browser sounds a bit crazy.
Server (ie author)-side rendering looks much simpler and faster. You don't want you browser to reflow a commutative diagram anyway.
How many commutative diagrams do we have in the docstrings right now?
Okay, I found a bit more time to work on this. Here's a refresh. Maybe the colors are more to Patrick's taste. https://robertylewis.com/mathlib_docs/
This builds with @Wojciech Nawrocki 's additions to 3.5c, so it can display module docs used to section a file. I don't think we have any of these in mathlib yet, but here's a demo: https://robertylewis.com/mathlib_docs/topology/whoa.html
The font for theorem statements is a bit large (being used also as the header). Most statements don't fit on one line, and a decent fraction of them seem to have the line break exactly where things get interesting
One possibility is to remove all implicit and instance implicit arguments from the main display, and put them in smaller type afterward
Nice work! Starts to look really good. I agree with Mario's points though.
Also, you might try to detect unnamed hypotheses by type so that you can turn more arguments into arrows (especially arguments named a_1
, a_2
that were arrows to begin with)
Sure, it's easy enough to change the font sizes. The line breaks will obviously depend on how wide your window is. This can be fiddled with.
One possibility is to remove all implicit and instance implicit arguments from the main display, and put them in smaller type afterward
Not sure exactly what you have in mind with "put them in smaller type afterward." Do you mean state the type twice, once without implicits and once with?
Also, you might try to detect unnamed hypotheses by type so that you can turn more arguments into arrows (especially arguments named
a_1
,a_2
that were arrows to begin with)
What's the robust way to do this? In effect, "intros until the last named argument."
not sure if it's better to quote just the omitted implicits or the full type. I was thinking something like:
theorem add_monoid.zero_smul (a : β) :
add_monoid.smul 0 a = 0
@[simp]
; {β : Type u} [add_monoid β]
If you have expr info, you can check whether a variable appears in the body to determine if it can be "arrowed"
there is an expr function for this
expr.is_arrow
which uses expr.has_var
I don't feel strongly about how much lean syntax to use in these displays. I and many others will be used to it, but I would also be happy with something that reimagines the syntax a bit or puts more things in a prose style
not sure if it's better to quote just the omitted implicits or the full type. I was thinking something like:
- Line 1 (header):
theorem add_monoid.zero_smul (a : β) :
- Line 2 (main text):
add_monoid.smul 0 a = 0
- Line 3 (footnote size):
@[simp]
;{β : Type u} [add_monoid β]
Hmm. This hides the information about where the implicits appear in the signature. Usually you don't need to know this but sometimes you do, and it limits how useful the docs are if they don't give it. What about a javascript toggle to flip between "all variables" and "explicit only"? "explicit only" could be the default.
I hate to suggest more javascript work for me to do, but it would look nice.
expr.is_arrow
Ah, right. I think I can do this easily.
I know that this makes exact implicit order not visible, but I think that's a tolerable tradeoff. We already have methods like #print
or hovers for getting this kind of info from a definition, and we're already not sharing some information that might be relevant, like the definition or proof itself
If you want to have a JS toggle for this, I wouldn't mind it though
For a much harder problem, I would really like to see some proof displays. I have gotten a lot of value out of the metamath web pages that give super detailed proofs of anything you could hope for, and it would be great if lean had anything half as good
I think the best kind of proof display we'll have in the near future is the current "click the declaration name to go to the source on GitHub." It doesn't seem helpful to display full proof terms. And adding any sort of interactivity to a displayed proof script seems... challenging.
Like I said, it's not an easy problem. I can dream though
I actually do want to see full proof terms, just not in the horrible way pp.all
does it
interactivity opens up a huge number of possibilities here, and the space is certainly not well explored
Fair enough. For a really good display I'm not sure even the proof term is enough. My dream interactive browser would note when a proof term was generated by a certain tactic. I agree it's not well explored, but it would take a lot of exploring to get to something really useful.
You certainly need the types of subterms. There is probably a way to turn such information into something like an evolving tactic state
you are right that recovering provenance data is hard to impossible and also pretty valuable (although not the whole story). I always felt cheated when I went through an isabelle tutorial and everything was by auto
. I wasn't any closer to understanding why fact X is true, and the computer didn't know how to communicate why
Maybe the colors are more to Patrick's taste.
If they're not then you can tell him to fix it up himself ;-) They look fine to me! (but then again I guess you could question my tastes in colours...)
What is doable is to diplay the proof taken from the Lean file, with tactic state as it appears in VScode. This is what is done by format_lean.
that doesn't solve the by auto
problem though (or by tidy
in our case)
Sure, but it would already be a huge improvement.
true
you are right that recovering provenance data is hard to impossible and also pretty valuable (although not the whole story). I always felt cheated when I went through an isabelle tutorial and everything was
by auto
. I wasn't any closer to understanding why fact X is true, and the computer didn't know how to communicate why
The problem is that sometimes the answer to "why" is "by auto," and sometimes the answer is what auto did, so you you need the option to see both.
This reminds me of Lamport's structured proofs https://lamport.azurewebsites.net/pubs/proof.pdf
Okay. It's updated to print implicit arguments below, and to prefer arrows in the type to named arrows when that makes sense. I still have all the data so it won't be hard to create a JS toggle to show the full type. The hardest thing there will be where to put the button.
@Gabriel Ebner pointed out a big benefit of making these docs public, even though they're in an early state: they make it much easier to notice doc strings that are missing, wrong, malformed, etc. So I've put them up at an "official" location. https://leanprover-community.github.io/mathlib_docs/
I don't know how well the search will work. We need to wait for Google to index the docs before it will work at all.
At some point we'll want to regenerate them daily. I think it's probably best to do this as part of the Travis build that updates lean-3.4.2
, but maybe it's better to use @Scott Morrison 's server?
I love that the first doc string I looked at was this one: https://github.com/leanprover-community/mathlib/blob/3f9c4d886493afe2dbaada17d25e486b1872e047/src/algebra/associated.lean#L13
There's, uh, a big range of doc string quality in the library right now...
Unfortunately we can't (yet) have a linter for that. The problem is NLP-complete...
On the other side of things from is unit
are @Sebastien Gouezel 's files. https://leanprover-community.github.io/mathlib_docs/geometry/manifold/manifold.html
@Rob Lewis Here's a little comment: consider https://leanprover-community.github.io/mathlib_docs/geometry/manifold/smooth_manifold_with_corners.html
I think the stuff under main definitions is typeset as a list in the source code. Is there some markdownish reason why that didn't happen here?
I guess https://github.com/leanprover-community/mathlib/blob/3f9c4d886493afe2dbaada17d25e486b1872e047/src/geometry/manifold/smooth_manifold_with_corners.lean#L24-L36 is not interpreted as a list by markdown
Because it's not actually typeset as a list.
Each item should start with *
or -
or something.
Yes, my mistake, I did not write it using proper markdown (as I was not aware at the time that real markdown would be relevant).
This is why I wanted to publicize the HTML docs. These things are impossible to see in the Lean files, but obvious when you see them in action.
What is the reason that times_cont_diff_groupoid
is hyperlinked in that blob of text, but other names are not?
Because that's the full name. The other things have namespaces in front of them.
Ach so
I don't think there's any way around this, the name resolution would be ambiguous.
Actually -- in this case that might not be the issue, smooth_manifold_with_corners
isn't namespaced.
Not sure why that's failing to link. I'll look into it soon.
With the power of Observable, I've written a tool that renders all the markdown docstrings in a Lean file on GitHub. You can also paste in the URL to a PR (or even just the number of a PR to mathlib) and all the docstrings in the changed Lean files will be displayed. I hope this will be useful for mathlib PR reviewers or contributors who want to check the markdown in their docstrings.
Note that I'm not able to show the declaration (with the name / type) corresponding to the docstring at the moment. Also, the tool relies on marked
so some things may appear slightly different from mathlib_docs, which uses markdown2. Let me know if there's anything I can change to make it easier to use!
Another example: This presentation of Isabelle/ZF theories is quite nice.
The docs are updated, thanks largely to @Gabriel Ebner ! https://leanprover-community.github.io/mathlib_docs/geometry/manifold/manifold.html
New features include prettier styling, collapsible display of implicit arguments, linked notation, and lists of class instances (see the collapsible list at https://leanprover-community.github.io/mathlib_docs/algebra/module.html#module).
IMHO, this is absolutely awesome. Clicking around a bit I wonder if it would be worth styling the links to GH source differently from the links to elsewhere in the docs.
Anyway, great work.
An early Christmas present for you all: I've added some of the mathlib doc files (#1815) to the doc display. https://leanprover-community.github.io/mathlib_docs/tactic_writing.html
This is work in progress, the menus on the left aren't quite right yet.
And, of course, the doc files themselves need updating.
But there won't be much progress here for the next few weeks, so it's up for now!
This is so cool. Our library is growing up :D
I have a small contribution to mathlib docs website effort. I tried to fix CSS so I can use it on my phone. I modified one sample page and put it at https://www.math.u-psud.fr/~pmassot/test/. Please test on various screen sizes (but beware that clicking any link will bring you to the current website). @Rob Lewis you can diff the html and CSS against the current website, changing the documentation generator should be extremely easy. This is minimal modification that, on screens narrower than 1000px, removes the left side bar and collapse the right one with a menu button on a sticky header.
Thanks! I don't have time now, but I'll play around with it. The fixed "Lean mathlib docs" header looks a little funny on a wide screen, especially how it pushes the scroll bars and search windows down. It'll take some fiddling.
This is very easy to fix. I just pushed a version which hides that header on wide screens. I guess we could instead give it a different background color, or put more stuff in it.
Patrick, I haven't forgotten about your contribution. But the mobile friendly version still looks off on my non-mobile screens and I haven't found the energy to dive back into the CSS yet.
I hope I'll be able to resume work on this next week (not before Wednesday though). Your recent work should make it easier for me to try things, but it would help to tell me more precisely what "looks off".
{% endraw %}Last updated: Apr 24 2020 at 19:02 UTC


A directive for handling basic html events (e.g., blur, keyup, focus, etc.)
Currently MacGyver has blur, focus, keydown, keyup, mouseenter and mouseleave
mac-blur
Type: Expression
Expression to evaluate on blur
mac-focus
Type: Expression
Expression to evaluate on focus
mac-keydown
Type: Expression
Expression to evaluate on keydown
mac-keyup
Type: Expression
Expression to evaluate on keyup
mac-mouseenter
Type: Expression
Expression to evaluate on mouseenter
mac-mouseleave
Type: Expression
Expression to evaluate on mouseleave


- Facebook page for DDraceNetwork, maintained by onionly .me'
- DDNet Chile running on a new server with new IP now
- DDNet RUS running on a new server with new IP now
- DDNet 8.1.1:
- [Client] Add country flags for Europe and Catalonia
- [Client] Bind chat on enter/return by default as well
- [Client] Dyncam bind saves special mousesens (by Shiki)
- [Client] Sort spectators by name in scoreboard
- [Client] Add friends and foes commands to list them in console
- [Client] Make clan optional when adding and removing friends and foes
- [Client] Fix: Only print MOTD to console when it's not empty
- [Server] Show average time in /mapinfo
- [Mapping] Add basic_freeze automappers (by hi_leute_gll and DoNe)
- [Mapping] Add generic_clear automappers (by hi_leute_gll)
- [Mapping] Fix desert_mountains_new_foreground (by hi_leute_gll)
- If you're running Windows 10 and are experiencing lags in DDNet, you should disable Windows Update P2P
- DDNet 8.0.2:
- [Client] Fix saving of config file on Windows
- [Client] Fix and improve spectator mode in demo viewer
- [Client] Print MOTD to the console
- [Mapping] Add basic_freeze automapper rules (by DoNe)
- DDNet 8.0:
- [Client] Allow spectating other players and freeview in demo player (especially fun with /showall and /showothers on)
- [Client] Add foes feature to permanantly ignore players (F1, add_foe only)
- [Client] Use temporary file for saving config to prevent broken configs
- [Client] Fix: Make add_demomarker working in all recorders (by east)
- [Client] Fix highlighting in demo playback (by east)
- [Client] Fix: TAB in console doesn't influence server browser
- [Client] Fix scroll bar in server control votes when search bar is used
- [Server] Add switch_open to set the initial state of a switch to open
- [Server] Fix support for 0 stars in database
- [Server] Fix /mapinfo with mixed case server names (DDmaX)
- [Editor] Fix envelope button color (by DoNe)
- [Editor] Save twice as fast (hopefully doesn't break anything)
- [Editor] Add "Save copy" button so that filename is not changed
- [Editor] Add ctrl+shift+s for "save as" and ctrl+shift+alt+s for "save copy"
- [Editor] Zoom faster by holding down numpad +/- (by Chairn)
- The History of DDNet
- DDNet 7.9.1:
- [Client] Show all recorders at top of scoreboard
- [Client] Sort players in server browser by name too
- [Client] Fix statboard for some resolutions
- [Client] Fix saving of favorite IPv6 servers (by east)
- [Client] Fix demo cutter to add .demo file ending
- [Client] Improved German translations (by DoNe)
- [Mapping] Add many nice mapres to the client (thanks to Soreu)
- [Mapping] Improved grass_main/0.7 automappers (by hi_leute_gll)
- [Mapping] Rename mapres to have consistent names
- [Editor] Scroll speedup angles by 45° (finer with shift)
- [Editor] Fix: Show degrees sign in values selector
- [Server] Veto right for players with high time (20 minutes) to stop map change votes
- [Server] Only allow /save when team is started already to prevent saving after noobfilter
- [Server] Make /map and /mapinfo work for maps with really similar names
- [Server] Show nice messages to known bot clients
- [Server] Fix /map and /mapinfo with special unicode characters
- [Server] Fix: Only disallow team changing/killing when calling kick/spec votes
- [Server] Fix: Vote callers never count as afk
- [Compilation] Use system libraries by default when available (should enable building DDNet on any platform and OS)
- DDNet Persian is returning thanks to KinG and Persian Tee City Staff!
- DDNet South Africa on new host!
After we had lots of connection problems on our last host, we now have a new server in South Africa, thanks to lordtheuns!
- DDNet Funding


Issue: PACKAGE-FUNCTION-CONSISTENCYReferences: 11.7 Package System Functions and Variables (pp182-188)
Category: CLARIFICATION/CHANGE
Edit history: 21-Oct-88, Version 1 by Pitman
12-Jan-89, Version 2 by Masinter (add MORE-PERMISSIVE option)
17-Mar-89, Version 3, by Masinter, MORE-PERMISSIVE as
amended & adopted at Jan 89 X3j13
17-Mar-89, Version 4, by Moon, correct amended wording
Problem Description:
CLtL is vague about whether either or both of package or package name
are permissible in some cases.
Proposal (PACKAGE-FUNCTION-CONSISTENCY:MORE-PERMISSIVE):
Clarify that it is permissible to pass either a package object
or a package name (symbol or string) in the following situations:
- the :USE argument to MAKE-PACKAGE or IN-PACKAGE
- the first argument to IN-PACKAGE, FIND-PACKAGE, RENAME-PACKAGE
- the second argument to INTERN, FIND-SYMBOL, UNINTERN
- the second argument to EXPORT, UNEXPORT, IMPORT,
SHADOWING-IMPORT, and SHADOW
- the first argument (or a member of the list which is the first
argument) to USE-PACKAGE or UNUSE-PACKAGE.
- all package-name arguments in DEFPACKAGE except for the name and
nicknames of the package being defined.
- the first argument to PACKAGE-NAME, PACKAGE-NICKNAMES,
PACKAGE-USE-LIST, or PACKAGE-USED-BY-LIST
- the PACKAGE argument to DO-SYMBOLS.
- the PACKAGE argument to DO-EXTERNAL-SYMBOLS.
- the PACKAGE argument to DO-ALL-SYMBOLS.
If FIND-PACKAGE is given a package object as an argument, it simply
returns it.
Clarify that the function MAKE-PACKAGE permits only a package name
as an argument since it does not make sense to create an existing
package.
Clarify that package nicknames must always be expressed as package
names (symbols or strings) and may never be actual package objects.
In the list above, IN-PACKAGE may be changed to SELECT-PACKAGE
if IN-PACKAGE-FUNCTIONALITY:NEW-MACRO passes.
Examples:
(INTERN "FOO" "KEYWORD") => :FOO
(DEFVAR *FOO-PACKAGE* (MAKE-PACKAGE "FOO"))
(RENAME-PACKAGE "FOO" "FOO0")
(PACKAGE-NAME *FOO-PACKAGE*) => "FOO0"
(PACKAGE-NAME "SYS") might return "SYSTEM".
Rationale:
This makes things more consistent.
It also adds a generally useful capability.
Current Practice:
Symbolics Genera & Lucid permit strings as package names.
Symbolics Cloe does not permit strings as package names.
In Lucid FIND-PACKAGE and IN-PACKAGE require names.
Cost to Implementors:
Small.
Cost to Users:
None. This change is upward compatible.
Cost of Non-Adoption:
Implementations would continue to vary gratuitously, leaving a potential
for portability problems.
Benefits:
The cost of non-adoption is avoided.
Aesthetics:
This makes things more regular, and so presumably more aesthetic.
Discussion:
Pitman ran across this problem while trying to port Macsyma to various
implementations. Discussion with other maintainers of portable programs
shows this is a common source of aggravation in portable code.
It would be possible to say that MAKE-PACKAGE took package objects as
arguments and just returned that package. That might have limited
usefulness on rare occasions, but mostly seemed too far out in left
field to bother suggesting it.


|
Interface Summary |
| AsmStmt |
The C front of COINS accepts following asm statement:
asm("#param paramDecsriptionList \n"
"#clobber destroyed-register-list \n"
asmInstructionSequence ,
actual-parameter-list );
where
paramDescriptionList -> paramDescription
| paramDescriptionList , paramDescription
paramDescription ->
%register // input parameter variable (rvalue)
| w%register // output parameter variable (lvalue)
| m%register // input/output parameter variable (lvalue)
| s // constant representing static address
| a // constant repreZsenting automatic variable address
destroyed-register-list -> %register // register contents is destroyed
| destroyed-register-list , %register
asmInstructionSequence ->
"asmInstruction \n"
| asmInstructionSequence "asmInstruction \n"
actualParameterList ->
expression // expression representing actual parameter
| actualParameterList , expression
The %register represents a register or a class of registers
defined in the TMD. |
| AssignStmt |
Assign-statement. |
| BlockStmt |
Block representing a sequence of statements. |
| ConstNode |
Constant node |
| ElemNode |
Element name node. |
| Exp |
Exp interface
HIR Exp class interface. |
| ExpListExp |
ExpListExp
Interface for the expression representing a list of expressions (Exp). |
| ExpStmt |
ExpStmt
Expression treated as a statement. |
| ForStmt |
For-statement interface. |
| FunctionExp |
FunctionExp
Function call interface. |
| HIR |
HIR interface
|
| HIR0 |
HIR0 interface
|
| HirIterator |
HirIterator interface
Traverse HIR node in depth first order. |
| HirList |
HirList interfac
|
| HirSeq |
HirSeq interface
|
| HirVisitor |
HirVisitor
Visitor for processing HIR nodes |
| IfStmt |
If-statement. |
| IndexedLoopStmt |
IndexedLoop-statement interface. |
| InfNode |
Information list node
(pragma, comment line, etc.)
See IR. |
| InfStmt |
Information node treated as a statement
(pragma, comment line, etc.)
See IR. |
| JumpStmt |
JumpStmt interface |
| LabelDef |
Label definition |
| LabeledStmt |
LabeledStmt Labeled statement interface |
| LabelNode |
LabelNode: Label reference node. |
| LoopStmt |
LoopStmt -> // Loop statement is either for-loop, while-loop,
// repeat-loop, indexed loop, or other general loop. |
| NullNode |
Null node interface |
| PhiExp |
PhiExp
Phi expression interface. |
| PointedExp |
Pointed variable interface. |
| Program |
Program interface |
| QualifiedExp |
Qualified variable interface. |
| RepeatStmt |
Repeat-while-statement (do-while, repeat-until) interface. |
| ReturnStmt |
|
| SetDataStmt |
SetDataStmt interface
|
| Stmt |
Stmt
Stmt (statement) class interface. |
| SubpDefinition |
Subprogram definition node. |
| SubpNode |
Subprogram name node. |
| SubscriptedExp |
Subscripted variable interface. |
| SwitchStmt |
switch statement interface. |
| SymNode |
Symbol node |
| TypeNode |
Type name node interface. |
| UntilStmt |
Until-statement (do-while, repeat-until) interface. |
| VarNode |
Variable name node. |
| WhileStmt |
While-statement interface. |
|
Class Summary |
| AsmStmtImpl |
Asm node is treated as a statement. |
| AssignStmtImpl |
Assignment statement class. |
| BlockStmtImpl |
Block representing a sequence of statements. |
| ConstNodeImpl |
Constant node |
| ElemNodeImpl |
Element name node class. |
| ExpImpl |
ExpImpl
HIR expression class. |
| ExpListExpImpl |
ExpListExpImpl
Expression representing a list of expressions (Exp). |
| ExpStmtImpl |
ExpStmtImpl
Expression treated as a statement. |
| ForStmtImpl |
For-statement class. |
| FunctionExpImpl |
FunctionExpImpl
Function call expression. |
| HIR_Impl |
HIR_Impl class |
| HirAnnex |
class HirAnnex
Additional information that is not given in some case
and not given to some nodes. |
| HirIteratorImpl |
HirIteratorImpl class
Traverse HIR node in depth first order. |
| HirListImpl |
class HirListImpl
List of expressions, symbols, and others. |
| HirModify |
HirModify class
This class contains methods to modify HIR tree. |
| HirSeqImpl |
class HirSeqImpl
Sequence of expressions, symbols, and others. |
| HirVisitorModel1 |
HirVisitorModel1
Visitor model for processing HIR nodes where
visiting procedure is written in the method visit of this class
and each method of the form atXxx called from acceptor of HIR class
does a processing without writing traverse procedure. |
| HirVisitorModel2 |
HirVisitorModel2
Visitor model for processing HIR nodes where
each acceptor calls visitChildren method to traverse its children. |
| IfStmtImpl |
If-statement class. |
| IndexedLoopStmtImpl |
IndexedLoop-statement class. |
| InfNodeImpl |
Information list node (pragma, comment line, etc.) |
| InfStmtImpl |
Information node treated as a statement (pragma, comment line, etc.) |
| JumpStmtImpl |
JumpStmt class |
| LabelDefImpl |
Label definition |
| LabeledStmtImpl |
LabeledStmtImpl Labeled statement class |
| LabelNodeImpl |
Label reference node. |
| LoopStmtImpl |
Loop-statement class. |
| NullNodeImpl |
Null node |
| PhiExpImpl |
PhiExpImpl
Phi expression class. |
| PointedExpImpl |
Pointed variable class. |
| PrintStmtVisitor |
PrintStmtVisitor
Example of the use of Visitor for printing HIR statement
(Extends HirVisitorModel1.) |
| PrintVisitor |
PrintVisitor
Visitor for printing HIR
(Example of extending HirVisitorModel2.) |
| ProgramImpl |
ProgramImpl class |
| QualifiedExpImpl |
Qualified variable class. |
| RepeatStmtImpl |
Repeat-statement (do-while, repeat-until) class. |
| ReturnStmtImpl |
Return statement. |
| SetDataStmtImpl |
SetDataStmtImpl class
Specify initial values in the form
(setData l-value valueSpec) |
| SimplifyHir |
SimplifyHir:
|
| StmtImpl |
Statement |
| SubpDefinitionImpl |
Subprogram definition node. |
| SubpNodeImpl |
Subprogram name node. |
| SubscriptedExpImpl |
Subscripted variable class. |
| SubsPtrTransformation |
SubsPtrTransformation
Array subscript (Subs) expression to pointer expression transformation
and vice versa. |
| SwitchModify |
switch modify class. |
| SwitchStmtImpl |
switch statement class. |
| SymNodeImpl |
Symbol node |
| TestHir |
TestHir class
|
| TestHir2 |
Example of using HirVisitorModel2. |
| TypeNodeImpl |
Type name node class. |
| UntilStmtImpl |
Until-statement (do-while, repeat-until) class. |
| VarNodeImpl |
Variable name node class. |
| WhileStmtImpl |
While-statement class. |